perm filename WILSON.PRO[BMP,SYS]1 blob
sn#737808 filedate 1984-01-17 generic text, type T, neo UTF8
January 17, 1984 22:37:45
(NOTE-LIB RSA.LIB RSA.LISP)
[ 27.757015 0.0 ]
#FILE-IN-|DSK:RSA.LIB[BM,CLT]|-71766
(DEFN INVERSE
(J P)
(IF (EQUAL P 2.)
(REMAINDER J 2.)
(REMAINDER (EXP J (DIFFERENCE P 2.))
P)))
Note that (NUMBERP (INVERSE J P)) is a theorem.
[ 3.15901694 8.984375E-3 ]
INVERSE
(PROVE-LEMMA INVERSE-INVERTS-LEMMA
(REWRITE)
(IMPLIES (NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
(REMAINDER (EXP J (SUB1 P)) P))))
This formula can be simplified, using the abbreviations ZEROP, NOT,
and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0)) (NUMBERP P))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
(REMAINDER (EXP J (SUB1 P)) P))).
This simplifies, applying DIFFERENCE-1 and COMMUTATIVITY-OF-TIMES,
and expanding DIFFERENCE, EQUAL, NUMBERP, SUB1, and INVERSE, to the
following two new goals:
Case 2. (IMPLIES
(AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2)))
(EQUAL
(REMAINDER (TIMES J
(REMAINDER (EXP J (SUB1 (SUB1 P))) P))
P)
(REMAINDER (EXP J (SUB1 P)) P))),
which again simplifies, rewriting with TIMES-MOD-1, and expanding
the function EXP, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (TIMES J (EXP J (SUB1 (SUB1 P))))
P)
(REMAINDER 1 P))),
which we again simplify, rewriting with the lemmas EXP-BY-0,
TIMES-1, COMMUTATIVITY-OF-TIMES, and REMAINDER-OF-1, and unfolding
the function SUB1, to the following four new formulas:
Case 2.4.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0)
(NOT (EQUAL P 1))
(NOT (NUMBERP J)))
(EQUAL (REMAINDER 0 P) 1)).
But this again simplifies, using linear arithmetic, to:
T.
Case 2.3.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0)
(NOT (EQUAL P 1))
(NUMBERP J))
(EQUAL (REMAINDER J P) 1)),
which again simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0)
(EQUAL P 1)
(NOT (NUMBERP J)))
(EQUAL (REMAINDER 0 P) 0)),
which we again simplify, unfolding the functions EQUAL, NUMBERP,
SUB1, and REMAINDER, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0)
(EQUAL P 1)
(NUMBERP J))
(EQUAL (REMAINDER J P) 0)),
which we again simplify, applying REMAINDER-WRT-1, and expanding
the definitions of EQUAL, NUMBERP, and SUB1, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(EQUAL P 2))
(EQUAL (REMAINDER (TIMES J (REMAINDER J 2))
P)
(REMAINDER (EXP J (SUB1 P)) P))),
which we again simplify, rewriting with TIMES-MOD-1,
COMMUTATIVITY-OF-TIMES, TIMES-1, and EXP-BY-0, and unfolding the
definitions of EQUAL, NUMBERP, SUB1, and EXP, to the following two
new formulas:
Case 1.2.
(IMPLIES (NOT (NUMBERP J))
(EQUAL (REMAINDER (TIMES J J) 2)
(REMAINDER 0 2))),
which again simplifies, rewriting with the lemma TIMES-ZERO2, and
expanding the functions REMAINDER and EQUAL, to:
T.
Case 1.1.
(IMPLIES (NUMBERP J)
(EQUAL (REMAINDER (TIMES J J) 2)
(REMAINDER J 2))),
which again simplifies, applying COROLLARY-55, and opening up the
definition of PRIME, to:
(IMPLIES (AND (NUMBERP J)
(NOT (EQUAL (REMAINDER J 2) 0)))
(EQUAL (REMAINDER J 2) 1)),
which we again simplify, using linear arithmetic, rewriting with
LESSP-REMAINDER-DIVISOR, and expanding the definition of EQUAL,
to:
T.
Q.E.D.
[ 49.395052 0.78095703 ]
INVERSE-INVERTS-LEMMA
(PROVE-LEMMA INVERSE-INVERTS
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0.)))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
1.))
((USE (INVERSE-INVERTS-LEMMA))
(DISABLE INVERSE)))
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to the new conjecture:
(IMPLIES
(AND (IMPLIES (NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
(REMAINDER (EXP J (SUB1 P)) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
1)).
This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
FERMAT-THM, and expanding ZEROP, NOT, PRIME, IMPLIES, and EQUAL, to:
T.
Q.E.D.
[ 8.1670085 0.125992838 ]
INVERSE-INVERTS
(PROVE-LEMMA INVERSE-IS-UNIQUE
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL 1. (REMAINDER (TIMES M X) P)))
(EQUAL (INVERSE M P) (REMAINDER X P)))
((USE (INVERSE-INVERTS (J M))
(THM-55-SPECIALIZED-TO-PRIMES (Y (INVERSE M P))))))
WARNING: Note that the rewrite rule INVERSE-IS-UNIQUE will be stored
so as to apply only to terms with the nonrecursive function symbol
INVERSE.
WARNING: Note that INVERSE-IS-UNIQUE contains the free variable X
which will be chosen by instantiating the hypothesis:
(EQUAL 1. (REMAINDER (TIMES M X) P))
.
This formula can be simplified, using the abbreviations PRIME,
IMPLIES, and AND, to:
(IMPLIES
(AND
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (REMAINDER (TIMES (INVERSE M P) M) P)
1))
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M (INVERSE M P)) P))
(EQUAL (REMAINDER X P)
(REMAINDER (INVERSE M P) P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (INVERSE M P)
(REMAINDER X P))).
This simplifies, appealing to the lemmas DIFFERENCE-1,
COMMUTATIVITY-OF-TIMES, TIMES-MOD-1, and LESSP-REMAINDER2, and
expanding PRIME, NOT, AND, DIFFERENCE, EQUAL, NUMBERP, SUB1, INVERSE,
IMPLIES, REMAINDER, and PRIME1, to the following six new conjectures:
Case 6. (IMPLIES (AND (EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P))
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace M by
(PLUS Z (TIMES P V)) to eliminate (REMAINDER M P) and
(QUOTIENT M P). We rely upon LESSP-REMAINDER2, the type
restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to constrain
the new variables. We thus obtain the following two new formulas:
Case 6.2.
(IMPLIES (AND (NOT (NUMBERP M))
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P))
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))),
which further simplifies, rewriting with EQUAL-TIMES-0 and
TIMES-EQUAL-1, and opening up the functions LESSP, REMAINDER, and
EQUAL, to:
T.
Case 6.1.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(EQUAL Z 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1
(REMAINDER (TIMES (PLUS Z (TIMES P V)) X)
P))
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (EXP (PLUS Z (TIMES P V))
(SUB1 (SUB1 P)))
P)
(REMAINDER X P))).
However this further simplifies, rewriting with
ASSOCIATIVITY-OF-TIMES and REMAINDER-TIMES, and expanding NUMBERP,
EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
Case 5. (IMPLIES (AND (EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P))
(EQUAL P 2))
(EQUAL (REMAINDER M 2)
(REMAINDER X P))),
which we again simplify, using linear arithmetic and applying
LESSP-REMAINDER-DIVISOR, to:
(IMPLIES (AND (EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0)
(NOT (EQUAL 2 0))
(NUMBERP 2)
(NOT (EQUAL 2 1))
(PRIME1 2 (SUB1 2))
(EQUAL 1 (REMAINDER (TIMES M X) 2)))
(EQUAL 0 1)),
which we again simplify, opening up EQUAL, NUMBERP, SUB1, and
PRIME1, to:
(IMPLIES (AND (EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1
(REMAINDER (TIMES M X) 2)))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by
(PLUS Z (TIMES 2 V)) to eliminate (REMAINDER X 2) and
(QUOTIENT X 2). We rely upon LESSP-REMAINDER2, the type
restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to constrain
the new variables. We would thus like to prove the following four
new goals:
Case 5.4.
(IMPLIES (AND (NOT (NUMBERP X))
(EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1
(REMAINDER (TIMES M X) 2)))),
which further simplifies, opening up LESSP, NUMBERP, EQUAL, and
REMAINDER, to:
T.
Case 5.3.
(IMPLIES (AND (EQUAL 2 0)
(EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1
(REMAINDER (TIMES M X) 2)))).
This simplifies further, using linear arithmetic, to:
T.
Case 5.2.
(IMPLIES (AND (NOT (NUMBERP 2))
(EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1
(REMAINDER (TIMES M X) 2)))).
This simplifies further, trivially, to:
T.
Case 5.1.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (LESSP Z 2) (NOT (ZEROP 2)))
(NUMBERP V)
(NOT (EQUAL 2 0))
(EQUAL Z 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1
(REMAINDER (TIMES M (PLUS Z (TIMES 2 V)))
2)))).
This simplifies further, rewriting with the lemmas TIMES-2,
TIMES-1, COMMUTATIVITY-OF-TIMES,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, COMMUTATIVITY-OF-PLUS, and
COMMUTATIVITY2-OF-PLUS, and expanding the definitions of NUMBERP,
LESSP, ZEROP, NOT, and EQUAL, to the following two new
conjectures:
Case 5.1.2.
(IMPLIES
(AND (NUMBERP V)
(EQUAL (REMAINDER M 2) 0)
(NOT (NUMBERP M)))
(NOT (EQUAL 1
(REMAINDER (PLUS (TIMES M V)
(PLUS (TIMES M V) 0))
2)))).
But this finally simplifies, applying COMMUTATIVITY-OF-PLUS,
EQUAL-TIMES-0, and TIMES-EQUAL-1, and opening up the functions
LESSP, NUMBERP, EQUAL, REMAINDER, and PLUS, to:
T.
Case 5.1.1.
(IMPLIES
(AND (NUMBERP V)
(EQUAL (REMAINDER M 2) 0)
(NUMBERP M))
(NOT (EQUAL 1
(REMAINDER (PLUS (TIMES M V)
(PLUS (TIMES M V) M))
2)))).
But this simplifies finally, applying COMMUTATIVITY-OF-PLUS,
COMMUTATIVITY2-OF-PLUS, DIVIDES-PLUS-REWRITE1, and
PRIME-KEY-REWRITE, and opening up the definitions of PRIME and
EQUAL, to:
T.
Case 4. (IMPLIES
(AND
(NOT (EQUAL P 2))
(EQUAL
(REMAINDER (TIMES M
(REMAINDER (EXP M (SUB1 (SUB1 P))) P))
P)
1)
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))),
which we again simplify, applying TIMES-MOD-1, to the new
conjecture:
(IMPLIES
(AND (NOT (EQUAL P 2))
(EQUAL (REMAINDER (TIMES M (EXP M (SUB1 (SUB1 P))))
P)
1)
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, we now replace M by
(PLUS Z (TIMES P V)) to eliminate (REMAINDER M P) and
(QUOTIENT M P). We use LESSP-REMAINDER2, the type restriction
lemma noted when REMAINDER was introduced, and the type restriction
lemma noted when QUOTIENT was introduced to constrain the new
variables. This generates the following two new goals:
Case 4.2.
(IMPLIES
(AND (NOT (NUMBERP M))
(NOT (EQUAL P 2))
(EQUAL (REMAINDER (TIMES M (EXP M (SUB1 (SUB1 P))))
P)
1)
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))).
But this simplifies further, applying EQUAL-TIMES-0 and
TIMES-EQUAL-1, and expanding LESSP and REMAINDER, to:
T.
Case 4.1.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(NOT (EQUAL P 2))
(EQUAL (REMAINDER (TIMES (PLUS Z (TIMES P V))
(EXP (PLUS Z (TIMES P V))
(SUB1 (SUB1 P))))
P)
1)
(EQUAL Z 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1
(REMAINDER (TIMES (PLUS Z (TIMES P V)) X)
P)))
(EQUAL (REMAINDER (EXP (PLUS Z (TIMES P V))
(SUB1 (SUB1 P)))
P)
(REMAINDER X P))).
This simplifies further, rewriting with EXP-TIMES,
ASSOCIATIVITY-OF-TIMES, and REMAINDER-TIMES, and expanding the
functions NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
Case 3. (IMPLIES
(AND
(NOT (EQUAL P 2))
(EQUAL
(REMAINDER (TIMES M
(REMAINDER (EXP M (SUB1 (SUB1 P))) P))
P)
1)
(NOT (EQUAL (REMAINDER X P)
(REMAINDER (EXP M (SUB1 (SUB1 P)))
P)))
(NOT (EQUAL 1
(REMAINDER (TIMES M (EXP M (SUB1 (SUB1 P))))
P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(NOT (EQUAL 1
(REMAINDER (TIMES M X) P)))),
which we again simplify, applying the lemma TIMES-MOD-1, to:
T.
Case 2. (IMPLIES (AND (EQUAL P 2)
(EQUAL (REMAINDER (TIMES M (REMAINDER M 2))
P)
1)
(EQUAL (REMAINDER M 2) 0)
(EQUAL 1 (REMAINDER (TIMES M X) 2)))
(EQUAL 0 (REMAINDER X 2))).
But this simplifies again, using linear arithmetic, rewriting with
the lemma LESSP-REMAINDER-DIVISOR, and expanding the definition of
EQUAL, to:
(IMPLIES (AND (EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER (TIMES M 0) 2) 1)
(EQUAL (REMAINDER M 2) 0)
(EQUAL 1 (REMAINDER (TIMES M X) 2)))
(EQUAL 0 1)).
This simplifies again, rewriting with the lemmas
COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, and TIMES-EQUAL-1, and
expanding the functions LESSP, NUMBERP, EQUAL, and REMAINDER, to:
T.
Case 1. (IMPLIES (AND (EQUAL P 2)
(EQUAL (REMAINDER (TIMES M (REMAINDER M 2))
P)
1)
(NOT (EQUAL (REMAINDER X 2)
(REMAINDER M 2)))
(NOT (EQUAL 1
(REMAINDER (TIMES M M) 2))))
(NOT (EQUAL 1
(REMAINDER (TIMES M X) 2)))).
However this simplifies again, rewriting with the lemma TIMES-MOD-1,
to:
T.
Q.E.D.
[ 148.71097 1.64200847 ]
INVERSE-IS-UNIQUE
(PROVE-LEMMA S-P-I-I-LEMMA1
(REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1.)))
(EQUAL (TIMES (SUB1 N) (SUB1 N))
(PLUS 1. (TIMES N (SUB1 (SUB1 N)))))))
This formula can be simplified, using the abbreviations ZEROP, NOT,
AND, and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N) (SUB1 N))
(PLUS 1 (TIMES N (SUB1 (SUB1 N)))))).
This simplifies, unfolding the functions SUB1, NUMBERP, EQUAL, and
PLUS, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N) (SUB1 N))
(ADD1 (TIMES N (SUB1 (SUB1 N)))))).
Applying the lemma SUB1-ELIM, replace N by (ADD1 X) to eliminate
(SUB1 N) and X by (ADD1 Z) to eliminate (SUB1 X). We employ the type
restriction lemma noted when SUB1 was introduced to restrict the new
variable. We thus obtain two new formulas:
Case 2. (IMPLIES (AND (EQUAL X 0)
(NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL (ADD1 X) 1)))
(EQUAL (TIMES X X)
(ADD1 (TIMES (ADD1 X) (SUB1 X))))).
This further simplifies, clearly, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL (ADD1 (ADD1 Z)) 0))
(NOT (EQUAL (ADD1 (ADD1 Z)) 1)))
(EQUAL (TIMES (ADD1 Z) (ADD1 Z))
(ADD1 (TIMES (ADD1 (ADD1 Z)) Z)))),
which we further simplify, rewriting with the lemmas ADD1-EQUAL,
TIMES-ADD1, COMMUTATIVITY-OF-TIMES, SUB1-ADD1, PLUS-ADD1, and
COMMUTATIVITY2-OF-PLUS, and unfolding the functions NUMBERP and
PLUS, to:
T.
Q.E.D.
[ 2.5559896 0.248014323 ]
S-P-I-I-LEMMA1
(PROVE-LEMMA S-P-I-I-LEMMA2
(REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1.)))
(EQUAL (REMAINDER (TIMES (SUB1 N) (SUB1 N))
N)
1.))
((USE (S-P-I-I-LEMMA1)
(REMAINDER-PLUS-TIMES-2 (J N)
(X 1.)
(I (SUB1 (SUB1 N)))))
(DISABLE S-P-I-I-LEMMA1 REMAINDER-PLUS-TIMES-2)))
This formula can be simplified, using the abbreviations ZEROP, NOT,
IMPLIES, and AND, to the new conjecture:
(IMPLIES
(AND (IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N) (SUB1 N))
(PLUS 1 (TIMES N (SUB1 (SUB1 N))))))
(EQUAL (REMAINDER (PLUS 1 (TIMES N (SUB1 (SUB1 N))))
N)
(REMAINDER 1 N))
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (SUB1 N) (SUB1 N))
N)
1)).
This simplifies, rewriting with REMAINDER-OF-1, and opening up the
definitions of ZEROP, NOT, AND, SUB1, NUMBERP, EQUAL, PLUS, and
IMPLIES, to:
T.
Q.E.D.
[ 3.26298827 0.079003906 ]
S-P-I-I-LEMMA2
(PROVE-LEMMA SUB1-P-IS-INVOLUTION
(REWRITE)
(IMPLIES (PRIME P)
(EQUAL (INVERSE (SUB1 P) P) (SUB1 P)))
((USE (INVERSE-IS-UNIQUE (M (SUB1 P))
(X (SUB1 P))))
(DISABLE INVERSE)))
WARNING: Note that the rewrite rule SUB1-P-IS-INVOLUTION will be
stored so as to apply only to terms with the nonrecursive function
symbol INVERSE.
This formula can be simplified, using the abbreviations PRIME and
IMPLIES, to:
(IMPLIES
(AND (IMPLIES (AND (PRIME P)
(EQUAL 1
(REMAINDER (TIMES (SUB1 P) (SUB1 P))
P)))
(EQUAL (INVERSE (SUB1 P) P)
(REMAINDER (SUB1 P) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (INVERSE (SUB1 P) P)
(SUB1 P))).
This simplifies, using linear arithmetic, rewriting with
S-P-I-I-LEMMA1, REMAINDER-OF-1, REMAINDER-PLUS-TIMES-2,
REMAINDER-0-CROCK, and DIFFERENCE-0, and opening up the definitions
of PRIME, EQUAL, AND, REMAINDER, and IMPLIES, to:
(IMPLIES (AND ( LEQ P (SUB1 P))
(EQUAL (INVERSE (SUB1 P) P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL 0 (SUB1 P))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 2.2989746 0.200016277 ]
SUB1-P-IS-INVOLUTION
(PROVE-LEMMA N-O-I-LEMMA1
(REWRITE)
(EQUAL (DIFFERENCE (TIMES X X) 1.)
(TIMES (ADD1 X) (SUB1 X))))
This formula can be simplified, using the abbreviation DIFFERENCE-1,
to:
(EQUAL (SUB1 (TIMES X X))
(TIMES (ADD1 X) (SUB1 X))).
Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to
eliminate (SUB1 X). We rely upon the type restriction lemma noted
when SUB1 was introduced to restrict the new variable. This produces
the following three new goals:
Case 3. (IMPLIES (EQUAL X 0)
(EQUAL (SUB1 (TIMES X X))
(TIMES (ADD1 X) (SUB1 X)))),
which simplifies, unfolding the definitions of TIMES, SUB1, and
EQUAL, to:
T.
Case 2. (IMPLIES (NOT (NUMBERP X))
(EQUAL (SUB1 (TIMES X X))
(TIMES (ADD1 X) (SUB1 X)))).
This simplifies, applying TIMES-ZERO2, SUB1-TYPE-RESTRICTION, and
SUB1-NNUMBERP, and opening up SUB1, TIMES, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (SUB1 (TIMES (ADD1 Z) (ADD1 Z)))
(TIMES (ADD1 (ADD1 Z)) Z))),
which we simplify, rewriting with TIMES-ADD1,
COMMUTATIVITY-OF-TIMES, SUB1-ADD1, PLUS-ADD1, and
COMMUTATIVITY2-OF-PLUS, and unfolding the function PLUS, to:
T.
Q.E.D.
[ 2.0569987 0.163020832 ]
N-O-I-LEMMA1
(PROVE-LEMMA N-O-I-LEMMA2
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL (REMAINDER (DIFFERENCE (TIMES J J) 1.)
P)
0.))
(OR (EQUAL (REMAINDER (ADD1 J) P) 0.)
(EQUAL (REMAINDER (SUB1 J) P) 0.))))
WARNING: Note that the rewrite rule N-O-I-LEMMA2 will be stored so
as to apply only to terms with the nonrecursive function symbol OR.
This conjecture can be simplified, using the abbreviations OR, PRIME,
AND, IMPLIES, and N-O-I-LEMMA1, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (REMAINDER (TIMES (ADD1 J) (SUB1 J))
P)
0)
(NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
(EQUAL (REMAINDER (SUB1 J) P) 0)).
This simplifies, appealing to the lemma PRIME-KEY-REWRITE, and
expanding PRIME, to:
T.
Q.E.D.
[ 7.8189453 0.0600423175 ]
N-O-I-LEMMA2
(PROVE-LEMMA N-O-I-LEMMA3
(REWRITE)
(IMPLIES (AND ( LEQ 1. A)
(EQUAL (REMAINDER A P) 1.))
(EQUAL (REMAINDER (SUB1 A) P) 0.))
((USE (EQUAL-MODS-TRICK-2 (B 1.)))
(DISABLE N-O-I-LEMMA1)))
This conjecture simplifies, rewriting with the lemmas REMAINDER-OF-1
and REMAINDER-WRT-1, and unfolding the functions IMPLIES, SUB1,
NUMBERP, EQUAL, and LESSP, to:
(IMPLIES (AND (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by
(PLUS X (TIMES P Z)) to eliminate (REMAINDER A P) and (QUOTIENT A P).
We employ LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to restrict the new variables. We thus
obtain three new formulas:
Case 3. (IMPLIES (AND (EQUAL P 0)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0)).
This further simplifies, expanding the definitions of EQUAL,
REMAINDER, and SUB1, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which we further simplify, rewriting with REMAINDER-WRT-12 and
REMAINDER-0-CROCK, and unfolding the functions SUB1 and EQUAL, to:
T.
Case 1. (IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(EQUAL (REMAINDER (PDIFFERENCE (PLUS X (TIMES P Z)) 1)
P)
0)
(NOT (EQUAL (PLUS X (TIMES P Z)) 0))
(EQUAL X 1))
(EQUAL (REMAINDER (SUB1 (PLUS X (TIMES P Z)))
P)
0)).
However this further simplifies, appealing to the lemmas
REMAINDER-PLUS-TIMES-2, REMAINDER-OF-1, EQUAL-MODS-TRICK-2, and
PLUS-EQUAL-0, and unfolding the definitions of NUMBERP, ZEROP, NOT,
and EQUAL, to:
(IMPLIES (AND (LESSP 1 P)
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0)))
(EQUAL (REMAINDER (SUB1 (PLUS 1 (TIMES P Z)))
P)
0)),
which we would normally push and work on later by induction. But
if we must use induction to prove the input conjecture, we prefer
to induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let us consider:
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND ( LEQ 1 A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T).
We named this *1 above. Let us appeal to the induction principle.
Three inductions are suggested by terms in the conjecture. They
merge into two likely candidate inductions, both of which are
unflawed. So we will choose the one suggested by the largest number
of nonprimitive recursive functions. We will induct according to the
following scheme:
(AND (IMPLIES (ZEROP P) (P A P))
(IMPLIES (AND (NOT (ZEROP P)) (LESSP A P))
(P A P))
(IMPLIES (AND (NOT (ZEROP P))
( LEQ P A)
(P (DIFFERENCE A P) P))
(P A P))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and
the definition of ZEROP establish that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates
three new formulas:
Case 3. (IMPLIES (ZEROP P)
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND ( LEQ 1 A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T)),
which simplifies, applying REMAINDER-WRT-12 and REMAINDER-OF-1, and
expanding ZEROP, EQUAL, REMAINDER, IMPLIES, SUB1, NUMBERP, LESSP,
NOT, and AND, to two new conjectures:
Case 3.2.
(IMPLIES (AND (EQUAL P 0)
(NUMBERP A)
(EQUAL A 1)
(EQUAL (PDIFFERENCE A 1) 0)
(NOT (EQUAL A 0)))
(EQUAL (SUB1 A) 0)).
However this again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (NOT (NUMBERP P))
(NUMBERP A)
(EQUAL A 1)
(EQUAL (PDIFFERENCE A 1) 0)
(NOT (EQUAL A 0)))
(EQUAL (SUB1 A) 0)),
which we again simplify, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP P)) (LESSP A P))
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND ( LEQ 1 A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T)).
This simplifies, using linear arithmetic, applying the lemmas
REMAINDER-OF-1, REMAINDER-0-CROCK, and DIFFERENCE-0, and unfolding
ZEROP, REMAINDER, IMPLIES, SUB1, NUMBERP, EQUAL, LESSP, NOT, and
AND, to three new formulas:
Case 2.3.
(IMPLIES
(AND (NOT (EQUAL P 0))
(NUMBERP P)
(LESSP A P)
(LESSP A 1))
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND ( LEQ 1 A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T)),
which we again simplify, rewriting with the lemmas
REMAINDER-0-CROCK, REMAINDER-OF-1, and SUB1-NNUMBERP, and
expanding the definitions of SUB1, NUMBERP, EQUAL, LESSP,
PDIFFERENCE, IMPLIES, NOT, AND, and REMAINDER, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(LESSP A P)
( LEQ 1 A)
(NUMBERP A)
(EQUAL A 1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(LESSP (SUB1 A) P))
(EQUAL (SUB1 A) 0)).
This again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(LESSP A P)
( LEQ 1 A)
(EQUAL P 1)
(NUMBERP A)
(NOT (EQUAL A 0))
(EQUAL A 1)
(LESSP (SUB1 A) P))
(EQUAL (SUB1 A) 0)),
which again simplifies, clearly, to:
T.
Case 1. (IMPLIES
(AND
(NOT (ZEROP P))
( LEQ P A)
(IF
(IMPLIES
(EQUAL (REMAINDER (DIFFERENCE A P) P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE (DIFFERENCE A P) 1)
P)
0))
(IMPLIES (AND ( LEQ 1 (DIFFERENCE A P))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0))
T))
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND ( LEQ 1 A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T)),
which simplifies, applying REMAINDER-OF-1 and EQUAL-DIFFERENCE-0,
and opening up the definitions of ZEROP, IMPLIES, SUB1, NUMBERP,
EQUAL, LESSP, NOT, AND, and REMAINDER, to seven new goals:
Case 1.7.
(IMPLIES
(AND
(NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P A)
(NOT (EQUAL P 1))
(NOT (EQUAL (REMAINDER (PDIFFERENCE (DIFFERENCE A P) 1)
P)
0))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which we again simplify, applying the lemmas REMAINDER-OF-1 and
EQUAL-MODS-TRICK-2, and opening up the definition of EQUAL, to:
T.
Case 1.6.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P A)
( LEQ A P)
(EQUAL P 1)
(NOT (EQUAL (REMAINDER (DIFFERENCE A P) P)
0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which we again simplify, using linear arithmetic, to the formula:
(IMPLIES (AND (NOT (EQUAL 1 0))
(NUMBERP 1)
( LEQ 1 1)
( LEQ 1 1)
(NOT (EQUAL 1 0))
(NOT (EQUAL 1 0))
(NUMBERP 1)
(EQUAL (REMAINDER (DIFFERENCE 1 1) 1)
1))
(EQUAL (REMAINDER (SUB1 1) 1) 0)).
This simplifies again, expanding the functions EQUAL, NUMBERP,
LESSP, DIFFERENCE, and REMAINDER, to:
T.
Case 1.5.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P A)
( LEQ A P)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
0)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P A)
( LEQ A P)
(NOT (EQUAL P 1))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) P) 0)).
However this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
( LEQ A A)
( LEQ A A)
(NOT (EQUAL A 1))
(EQUAL (REMAINDER (DIFFERENCE A A) A)
1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) A)
0)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) A) 0)),
which again simplifies, using linear arithmetic, applying
DIFFERENCE-0 and REMAINDER-0-CROCK, and opening up the
definitions of LESSP and EQUAL, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P A)
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0)
(EQUAL P 1)
(NOT (EQUAL (REMAINDER (DIFFERENCE A P) P)
0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which we again simplify, applying DIFFERENCE-1 and
REMAINDER-WRT-1, and expanding the functions EQUAL, NUMBERP, SUB1,
and LESSP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P A)
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
0)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P A)
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0)
(NOT (EQUAL P 1))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, applying REMAINDER-OF-1 and
EQUAL-MODS-TRICK-2, and unfolding EQUAL and REMAINDER, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P A)
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0)
(NOT (EQUAL P 1))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) P) 0)).
Applying the lemmas DIFFERENCE-ELIM, SUB1-ELIM, and
REMAINDER-QUOTIENT-ELIM, replace A by (PLUS P X) to eliminate
(DIFFERENCE A P), X by (ADD1 Z) to eliminate (SUB1 X), Z by
(PLUS X (TIMES P V)) to eliminate (REMAINDER Z P) and
(QUOTIENT Z P), and X by (PLUS Z (TIMES P V)) to eliminate
(REMAINDER X P) and (QUOTIENT X P). We employ the type
restriction lemma noted when DIFFERENCE was introduced, the type
restriction lemma noted when SUB1 was introduced,
LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER
was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to constrain the new variables. This
generates the following two new formulas:
Case 1.1.2.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(EQUAL (PLUS Z (TIMES P V)) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P (PLUS P (PLUS Z (TIMES P V))))
(EQUAL (REMAINDER (SUB1 (PLUS Z (TIMES P V)))
P)
0)
(NOT (EQUAL P 1))
(EQUAL Z 1)
(NOT (EQUAL (PLUS P (PLUS Z (TIMES P V)))
0)))
(EQUAL (REMAINDER (SUB1 (PLUS P (PLUS Z (TIMES P V))))
P)
0)),
which further simplifies, using linear arithmetic, to:
T.
Case 1.1.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP V)
(NOT (EQUAL (ADD1 (PLUS X (TIMES P V)))
0))
(NOT (EQUAL P 0))
(NUMBERP P)
( LEQ P
(PLUS P (ADD1 (PLUS X (TIMES P V)))))
(EQUAL X 0)
(NOT (EQUAL P 1))
(EQUAL (REMAINDER (ADD1 (PLUS X (TIMES P V)))
P)
1)
(NOT (EQUAL (PLUS P (ADD1 (PLUS X (TIMES P V))))
0)))
(EQUAL
(REMAINDER (SUB1 (PLUS P (ADD1 (PLUS X (TIMES P V)))))
P)
0)),
which further simplifies, appealing to the lemmas PLUS-ADD1,
SUB1-ADD1, REMAINDER-X-X, and REMAINDER-PLUS-TIMES-2, and
opening up NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
That finishes the proof of *1. Q.E.D.
[ 74.901123 1.66888021 ]
N-O-I-LEMMA3
(PROVE-LEMMA N-O-I-LEMMA4
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0.))
(EQUAL (INVERSE J P) J))
(OR (EQUAL (REMAINDER (ADD1 J) P) 0.)
(EQUAL (REMAINDER (SUB1 J) P) 0.)))
((USE (INVERSE-INVERTS) (N-O-I-LEMMA2))
(DISABLE INVERSE N-O-I-LEMMA1)))
WARNING: Note that the rewrite rule N-O-I-LEMMA4 will be stored so
as to apply only to terms with the nonrecursive function symbol OR.
This formula can be simplified, using the abbreviations OR, NOT,
PRIME, IMPLIES, AND, and DIFFERENCE-1, to:
(IMPLIES
(AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
1))
(IMPLIES (AND (PRIME P)
(EQUAL (REMAINDER (SUB1 (TIMES J J)) P)
0))
(OR (EQUAL (REMAINDER (ADD1 J) P) 0)
(EQUAL (REMAINDER (SUB1 J) P) 0)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) J)
(NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
(EQUAL (REMAINDER (SUB1 J) P) 0)),
which simplifies, applying the lemma INVERSE-IS-UNIQUE, and unfolding
PRIME, NOT, AND, IMPLIES, and OR, to:
(IMPLIES (AND (EQUAL (REMAINDER (TIMES J J) P) 1)
(NOT (EQUAL (REMAINDER (SUB1 (TIMES J J)) P)
0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (REMAINDER J P) J)
(NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
(EQUAL (REMAINDER (SUB1 J) P) 0)).
This simplifies again, using linear arithmetic, applying
LESSP-TIMES-2 and N-O-I-LEMMA3, and opening up EQUAL, to:
T.
Q.E.D.
[ 33.4720216 0.165983073 ]
N-O-I-LEMMA4
(PROVE-LEMMA NO-OTHER-INVOLUTIONS
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J (SUB1 P))
(LESSP 1. J))
(NOT (EQUAL (INVERSE J P) J)))
((USE (N-O-I-LEMMA4))
(DISABLE INVERSE)))
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to:
(IMPLIES
(AND (IMPLIES (AND (PRIME P)
(AND (NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) J)))
(OR (EQUAL (REMAINDER (ADD1 J) P) 0)
(EQUAL (REMAINDER (SUB1 J) P) 0)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(LESSP 1 J))
(NOT (EQUAL (INVERSE J P) J))).
This simplifies, using linear arithmetic, applying REMAINDER-0-CROCK,
DIFFERENCE-0, and SUB1-ADD1, and expanding the definitions of PRIME,
LESSP, REMAINDER, NOT, AND, OR, IMPLIES, EQUAL, SUB1, and NUMBERP, to
two new goals:
Case 2. (IMPLIES (AND (NOT (EQUAL J 0))
( LEQ (SUB1 P) (SUB1 J))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))),
which we again simplify, using linear arithmetic, to:
(IMPLIES (AND (LESSP J 1)
(NOT (EQUAL J 0))
( LEQ (SUB1 P) (SUB1 J))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))).
This again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (NUMBERP J))
(LESSP J 1)
(NOT (EQUAL J 0))
( LEQ (SUB1 P) (SUB1 J))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))),
which we again simplify, trivially, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL J 0))
( LEQ P (SUB1 J))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))).
However this simplifies again, using linear arithmetic, to:
(IMPLIES (AND (LESSP J 1)
(NOT (EQUAL J 0))
( LEQ P (SUB1 J))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))),
which again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (NOT (NUMBERP J))
(LESSP J 1)
(NOT (EQUAL J 0))
( LEQ P (SUB1 J))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))).
This simplifies again, obviously, to:
T.
Q.E.D.
[ 7.15994465 0.30504557 ]
NO-OTHER-INVOLUTIONS
(PROVE-LEMMA I-O-I-LEMMA NIL
(EQUAL (SUB1 (TIMES (DIFFERENCE P 2.)
(DIFFERENCE P 2.)))
(TIMES (DIFFERENCE P 3.) (SUB1 P))))
This simplifies, appealing to the lemmas DIFFERENCE-1 and
COMMUTATIVITY-OF-TIMES, and expanding the functions SUB1, NUMBERP,
EQUAL, and DIFFERENCE, to four new formulas:
Case 4. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 0)))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
(SUB1 (SUB1 P))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))).
Appealing to the lemma SUB1-ELIM, we now replace P by (ADD1 X) to
eliminate (SUB1 P), X by (ADD1 Z) to eliminate (SUB1 X), and Z by
(ADD1 X) to eliminate (SUB1 Z). We rely upon the type restriction
lemma noted when SUB1 was introduced to restrict the new variable.
This produces the following two new goals:
Case 4.2.
(IMPLIES (AND (EQUAL Z 0)
(NUMBERP Z)
(NOT (EQUAL (ADD1 (ADD1 Z)) 0))
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (SUB1 (TIMES Z Z))
(TIMES (ADD1 Z) (SUB1 Z)))),
which further simplifies, unfolding the definitions of NUMBERP,
EQUAL, TIMES, and SUB1, to:
T.
Case 4.1.
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL (ADD1 (ADD1 (ADD1 X))) 0))
(NOT (EQUAL (ADD1 (ADD1 X)) 0)))
(EQUAL (SUB1 (TIMES (ADD1 X) (ADD1 X)))
(TIMES (ADD1 (ADD1 X)) X))).
This simplifies further, applying TIMES-ADD1,
COMMUTATIVITY-OF-TIMES, SUB1-ADD1, PLUS-ADD1, and
COMMUTATIVITY2-OF-PLUS, and opening up PLUS, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
(SUB1 (SUB1 P))))
(TIMES (SUB1 P) 0))),
which we again simplify, unfolding SUB1, TIMES, and EQUAL, to:
T.
Case 2. (IMPLIES (EQUAL P 0)
(EQUAL (SUB1 (TIMES 0 0))
(TIMES (SUB1 P) 0))).
But this again simplifies, unfolding the definitions of TIMES, SUB1,
and EQUAL, to:
T.
Case 1. (IMPLIES (NOT (NUMBERP P))
(EQUAL (SUB1 (TIMES 0 0))
(TIMES (SUB1 P) 0))),
which we again simplify, rewriting with SUB1-NNUMBERP, and opening
up TIMES, SUB1, and EQUAL, to:
T.
Q.E.D.
[ 2.2139974 0.263997395 ]
I-O-I-LEMMA
(PROVE-LEMMA INVERSE-OF-INVERSE
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0.)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P)))
((USE (I-O-I-LEMMA)
(EXP-MOD-IS-1 (M J)
(J (SUB1 P))
(I (DIFFERENCE P 3.))))))
WARNING: Note that the rewrite rule INVERSE-OF-INVERSE will be
stored so as to apply only to terms with the nonrecursive function
symbol INVERSE.
This conjecture can be simplified, using the abbreviations NOT, PRIME,
IMPLIES, and AND, to the new formula:
(IMPLIES
(AND
(EQUAL (SUB1 (TIMES (DIFFERENCE P 2)
(DIFFERENCE P 2)))
(TIMES (DIFFERENCE P 3) (SUB1 P)))
(IMPLIES
(EQUAL (REMAINDER (EXP J (SUB1 P)) P)
1)
(EQUAL (REMAINDER (EXP J
(TIMES (DIFFERENCE P 3) (SUB1 P)))
P)
1))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P))).
This simplifies, applying DIFFERENCE-1, COMMUTATIVITY-OF-TIMES,
FERMAT-THM, EXP-BY-0, REMAINDER-OF-1, and DIFFERENCE-0, and expanding
SUB1, NUMBERP, EQUAL, DIFFERENCE, PRIME, IMPLIES, INVERSE, LESSP,
TIMES, and PRIME1, to the following two new goals:
Case 2. (IMPLIES
(AND (NOT (EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
(SUB1 (SUB1 P))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
P)
1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(NOT (EQUAL P 2)))
(EQUAL (INVERSE (REMAINDER (EXP J (SUB1 (SUB1 P))) P)
P)
(REMAINDER J P))),
which again simplifies, using linear arithmetic, rewriting with
LESSP-REMAINDER-DIVISOR, S-P-I-I-LEMMA1, REMAINDER-EXP, EXP-EXP,
EXP-PLUS, EXP-BY-0, TIMES-1, COMMUTATIVITY-OF-TIMES, and
DIFFERENCE-1, and expanding the functions EXP, DIFFERENCE, EQUAL,
NUMBERP, SUB1, and INVERSE, to two new conjectures:
Case 2.2.
(IMPLIES
(AND (NOT (EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (PLUS 1
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P))))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
P)
1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(NOT (EQUAL P 2))
(NOT (NUMBERP J)))
(EQUAL
(REMAINDER (TIMES 0
(EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P))))))
P)
(REMAINDER J P))),
which we again simplify, unfolding LESSP, REMAINDER, and EQUAL,
to:
T.
Case 2.1.
(IMPLIES
(AND (NOT (EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (PLUS 1
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P))))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
P)
1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(NOT (EQUAL P 2))
(NUMBERP J))
(EQUAL
(REMAINDER (TIMES J
(EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P))))))
P)
(REMAINDER J P))),
which again simplifies, rewriting with COROLLARY-55, and opening
up the functions PRIME and EQUAL, to:
T.
Case 1. (IMPLIES
(AND (NOT (EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
(SUB1 (SUB1 P))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
P)
1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL P 2))
(EQUAL (INVERSE (REMAINDER J 2) P)
(REMAINDER J P))).
However this again simplifies, using linear arithmetic and
rewriting with LESSP-REMAINDER-DIVISOR, to:
(IMPLIES
(AND (EQUAL (REMAINDER J 2) 1)
(NOT (EQUAL (SUB1 2) 0))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 2))
(SUB1 (SUB1 2))))
(TIMES (SUB1 2)
(SUB1 (SUB1 (SUB1 2)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 2)
(SUB1 (SUB1 (SUB1 2)))))
2)
1)
(NOT (EQUAL 2 0))
(NUMBERP 2)
(NOT (EQUAL 2 1))
(PRIME1 2 (SUB1 2))
(NOT (EQUAL 1 0)))
(EQUAL (INVERSE 1 2) 1)),
which we again simplify, rewriting with EXP-BY-0, and expanding the
definitions of SUB1, EQUAL, TIMES, REMAINDER, NUMBERP, PRIME1, and
INVERSE, to:
T.
Q.E.D.
[ 57.5770183 0.53497721 ]
INVERSE-OF-INVERSE
(PROVE-LEMMA N-Z-I-LEMMA
(REWRITE)
(IMPLIES (AND (ZEROP I) (LESSP 1. P))
(EQUAL (INVERSE I P) 0.)))
WARNING: Note that the rewrite rule N-Z-I-LEMMA will be stored so as
to apply only to terms with the nonrecursive function symbol INVERSE.
This simplifies, applying the lemmas EXP-OF-0 and DIFFERENCE-1, and
expanding the definitions of ZEROP, DIFFERENCE, EQUAL, NUMBERP, SUB1,
REMAINDER, INVERSE, and LESSP, to seven new goals:
Case 7. (IMPLIES (AND (EQUAL I 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which we again simplify, using linear arithmetic, to the following
three new formulas:
Case 7.3.
(IMPLIES (AND (NOT (NUMBERP P))
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, expanding the definition of LESSP, to:
T.
Case 7.2.
(IMPLIES (AND (EQUAL (SUB1 P) 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which we again simplify, using linear arithmetic, to:
T.
Case 7.1.
(IMPLIES (AND (LESSP P 1)
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)).
However this simplifies again, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (EQUAL I 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (NUMBERP P)))
(EQUAL (REMAINDER 1 P) 0)).
However this again simplifies, opening up the function LESSP, to:
T.
Case 5. (IMPLIES (AND (EQUAL I 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL P 0))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (EQUAL I 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 (SUB1 P)) 0)))
(EQUAL (REMAINDER 0 P) 0)),
which we again simplify, rewriting with REMAINDER-0-CROCK, and
opening up EQUAL, to:
T.
Case 3. (IMPLIES (AND (NOT (NUMBERP I))
(LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (NUMBERP P)))
(EQUAL (REMAINDER (EXP I 0) P) 0)),
which again simplifies, expanding the definition of LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP I))
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL P 0))
(EQUAL (REMAINDER (EXP I 0) P) 0)),
which we again simplify, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (NUMBERP I))
(LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (EQUAL P 0))
(NUMBERP P))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
0)).
Applying the lemma SUB1-ELIM, replace P by (ADD1 X) to eliminate
(SUB1 P) and X by (ADD1 Z) to eliminate (SUB1 X). We rely upon the
type restriction lemma noted when SUB1 was introduced to restrict
the new variable. This produces two new conjectures:
Case 1.2.
(IMPLIES (AND (EQUAL X 0)
(NUMBERP X)
(NOT (NUMBERP I))
(LESSP 1 (ADD1 X))
(NOT (EQUAL (ADD1 X) 2))
(NOT (EQUAL (ADD1 X) 0)))
(EQUAL (REMAINDER (EXP I (SUB1 X)) (ADD1 X))
0)).
However this further simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (NUMBERP I))
(LESSP 1 (ADD1 (ADD1 Z)))
(NOT (EQUAL (ADD1 (ADD1 Z)) 2))
(NOT (EQUAL (ADD1 (ADD1 Z)) 0)))
(EQUAL (REMAINDER (EXP I Z) (ADD1 (ADD1 Z)))
0)),
which we further simplify, rewriting with SUB1-ADD1 and
ADD1-EQUAL, and expanding the functions SUB1, NUMBERP, EQUAL, and
LESSP, to:
(IMPLIES (AND (NUMBERP Z)
(NOT (NUMBERP I))
(NOT (EQUAL Z 0)))
(EQUAL (REMAINDER (EXP I Z) (ADD1 (ADD1 Z)))
0)),
which we would normally push and work on later by induction. But
if we must use induction to prove the input conjecture, we prefer
to induct on the original formulation of the problem. Thus we
will disregard all that we have previously done, give the name *1
to the original input, and work on it.
So now let us consider:
(IMPLIES (AND (ZEROP I) (LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
named *1. We will try to prove it by induction. There is only one
plausible induction. We will induct according to the following
scheme:
(AND (IMPLIES (OR (EQUAL P 0) (NOT (NUMBERP P)))
(P I P))
(IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(P I P))
(IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(P I (SUB1 P)))
(P I P))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definitions of OR and NOT inform us that the measure (COUNT P)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme leads to
the following four new conjectures:
Case 4. (IMPLIES (AND (OR (EQUAL P 0) (NOT (NUMBERP P)))
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)).
This simplifies, opening up the functions NOT, OR, ZEROP, and LESSP,
to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(OR (EQUAL 1 0) (NOT (NUMBERP 1)))
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)).
This simplifies, opening up the functions NOT, OR, EQUAL, and
NUMBERP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
( LEQ (SUB1 P) 1)
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)).
This simplifies, using linear arithmetic, to two new conjectures:
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP P))
(NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
( LEQ (SUB1 P) 1)
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
which we again simplify, opening up the functions NOT and OR, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP P)
(NOT (OR (EQUAL 2 0) (NOT (NUMBERP 2))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
( LEQ (SUB1 2) 1)
(ZEROP I)
(LESSP 1 2))
(EQUAL (INVERSE I 2) 0)),
which we again simplify, expanding the definitions of EQUAL,
NUMBERP, NOT, OR, SUB1, LESSP, ZEROP, INVERSE, and REMAINDER, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(EQUAL (INVERSE I (SUB1 P)) 0)
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
which we simplify, rewriting with the lemmas DIFFERENCE-1, EXP-OF-0,
REMAINDER-0-CROCK, EXP-BY-0, TIMES-1, and COMMUTATIVITY-OF-TIMES,
and opening up the definitions of NOT, OR, EQUAL, NUMBERP,
DIFFERENCE, SUB1, INVERSE, ZEROP, LESSP, REMAINDER, and EXP, to
three new conjectures:
Case 1.3.
(IMPLIES
(AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(EQUAL I 0)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which we again simplify, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES
(AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(EQUAL I 0)
(NOT (EQUAL P 2))
(NOT (EQUAL (SUB1 (SUB1 P)) 0)))
(EQUAL (REMAINDER 0 P) 0)).
This again simplifies, applying EXP-OF-0 and REMAINDER-0-CROCK,
and expanding the function EQUAL, to:
T.
Case 1.1.
(IMPLIES
(AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(NOT (NUMBERP I))
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
0)).
This again simplifies, expanding the definition of EXP, to two
new conjectures:
Case 1.1.2.
(IMPLIES
(AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(NOT (NUMBERP I))
(NOT (EQUAL P 2))
(NOT (EQUAL (SUB1 (SUB1 P)) 0)))
(EQUAL (REMAINDER (TIMES I
(EXP I (SUB1 (SUB1 (SUB1 P)))))
P)
0)).
But this simplifies again, rewriting with the lemma
EQUAL-TIMES-0, and expanding the definitions of LESSP and
REMAINDER, to:
T.
Case 1.1.1.
(IMPLIES
(AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(NOT (NUMBERP I))
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 36.0820966 1.12291667 ]
N-Z-I-LEMMA
(PROVE-LEMMA NON-ZEROP-INVERSE
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0.)))
(NOT (ZEROP (INVERSE J P))))
((USE (N-Z-I-LEMMA (I (INVERSE J P)))
(INVERSE-OF-INVERSE))
(DISABLE INVERSE)))
WARNING: Note that the rewrite rule NON-ZEROP-INVERSE will be stored
so as to apply only to terms with the nonrecursive function symbol
ZEROP.
This conjecture can be simplified, using the abbreviations NOT, PRIME,
IMPLIES, and AND, to the goal:
(IMPLIES (AND (IMPLIES (AND (ZEROP (INVERSE J P))
(LESSP 1 P))
(EQUAL (INVERSE (INVERSE J P) P) 0))
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0)))
(NOT (ZEROP (INVERSE J P)))),
which simplifies, using linear arithmetic, applying the lemmas
LESSP-REMAINDER-DIVISOR and N-Z-I-LEMMA, and expanding the
definitions of ZEROP, SUB1, NUMBERP, EQUAL, LESSP, AND, IMPLIES,
PRIME, and NOT, to:
T.
Q.E.D.
[ 5.980013 0.085009766 ]
NON-ZEROP-INVERSE
(PROVE-LEMMA B-I-LEMMA2
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0.))
(EQUAL (INVERSE J P) (SUB1 P)))
(EQUAL (REMAINDER J P) (SUB1 P)))
((USE (INVERSE-OF-INVERSE))
(DISABLE INVERSE)))
This conjecture can be simplified, using the abbreviations NOT, PRIME,
AND, and IMPLIES, to the new formula:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) (SUB1 P)))
(EQUAL (REMAINDER J P) (SUB1 P))).
This simplifies, applying SUB1-P-IS-INVOLUTION, and expanding PRIME,
NOT, AND, and IMPLIES, to:
T.
Q.E.D.
[ 4.0479981 0.067024739 ]
B-I-LEMMA2
(PROVE-LEMMA B-I-LEMMA1 NIL
(IMPLIES (LESSP 1. P)
(LEQ (INVERSE J P) (SUB1 P))))
This conjecture simplifies, rewriting with the lemma DIFFERENCE-1,
and unfolding the functions DIFFERENCE, EQUAL, NUMBERP, SUB1, and
INVERSE, to four new conjectures:
Case 4. (IMPLIES (AND (LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (NUMBERP P)))
( LEQ
(REMAINDER (EXP J 0) P)
(SUB1 P))).
However this again simplifies, opening up the definition of LESSP,
to:
T.
Case 3. (IMPLIES (AND (LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL P 0))
( LEQ
(REMAINDER (EXP J 0) P)
(SUB1 P))).
However this simplifies again, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (EQUAL P 0))
(NUMBERP P))
( LEQ
(REMAINDER (EXP J (SUB1 (SUB1 P))) P)
(SUB1 P))).
This simplifies again, using linear arithmetic and applying
LESSP-REMAINDER-DIVISOR, to:
T.
Case 1. (IMPLIES (AND (LESSP 1 P) (EQUAL P 2))
( LEQ (REMAINDER J 2) (SUB1 P))),
which again simplifies, using linear arithmetic, rewriting with
LESSP-REMAINDER-DIVISOR, and opening up EQUAL, to:
T.
Q.E.D.
[ 6.4160319 0.144970704 ]
B-I-LEMMA1
(PROVE-LEMMA BOUNDED-INVERSE
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP J (SUB1 P)))
(LESSP (INVERSE J P) (SUB1 P)))
((USE (B-I-LEMMA1) (B-I-LEMMA2))
(DISABLE INVERSE)))
WARNING: Note that the linear lemma BOUNDED-INVERSE is being stored
under the term (INVERSE J P), which is unusual because INVERSE is a
nonrecursive function symbol.
This conjecture can be simplified, using the abbreviations PRIME,
IMPLIES, and AND, to the new formula:
(IMPLIES
(AND (IMPLIES (LESSP 1 P)
(IF (LESSP (SUB1 P) (INVERSE J P))
F
T))
(IMPLIES (AND (PRIME P)
(AND (NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) (SUB1 P))))
(EQUAL (REMAINDER J P) (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P)))
(LESSP (INVERSE J P) (SUB1 P))).
This simplifies, using linear arithmetic, applying REMAINDER-0-CROCK,
DIFFERENCE-0, and N-Z-I-LEMMA, and expanding SUB1, NUMBERP, EQUAL,
LESSP, IMPLIES, PRIME1, PRIME, REMAINDER, NOT, AND, and ZEROP, to the
following three new goals:
Case 3. (IMPLIES (AND ( LEQ (INVERSE J P) (SUB1 P))
( LEQ P J)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P)))
(LESSP (INVERSE J P) (SUB1 P))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND ( LEQ (INVERSE J P) (SUB1 P))
(NOT (EQUAL (INVERSE J P) (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P)))
(LESSP (INVERSE J P) (SUB1 P))).
This again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND ( LEQ (INVERSE J P) (SUB1 P))
(EQUAL J (SUB1 P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P J)
(LESSP J J))
(LESSP (INVERSE J P) J)),
which we again simplify, using linear arithmetic, to:
T.
Q.E.D.
[ 13.7189778 0.188020833 ]
BOUNDED-INVERSE
(DEFN INVERSE-LIST
(I P)
(IF (ZEROP I)
NIL
(IF (EQUAL I 1.)
(CONS 1. NIL)
(IF (MEMBER I (INVERSE-LIST (SUB1 I) P))
(INVERSE-LIST (SUB1 I) P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition
of ZEROP establish that the measure (COUNT I) decreases according to
the well-founded relation LESSP in each recursive call. Hence,
INVERSE-LIST is accepted under the principle of definition. Note
that (OR (LITATOM (INVERSE-LIST I P)) (LISTP (INVERSE-LIST I P))) is
a theorem.
[ 4.3540039 0.0459960937 ]
INVERSE-LIST
(PROVE-LEMMA ALL-NON-ZEROP-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I (SUB1 P)))
(ALL-NON-ZEROP (INVERSE-LIST I P)))
((USE (NON-ZEROP-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
This formula simplifies, applying SUB1-NNUMBERP, and expanding the
definitions of PRIME, NOT, AND, ZEROP, IMPLIES, SUB1, EQUAL, LESSP,
INVERSE-LIST, and OR, to 12 new goals:
Case 12.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))),
which we again simplify, using linear arithmetic, to:
T.
Case 11.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP NIL)).
However this simplifies again, opening up the definitions of LESSP,
REMAINDER, EQUAL, and ALL-NON-ZEROP, to:
T.
Case 10.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP NIL)),
which we again simplify, rewriting with the lemma REMAINDER-0-CROCK,
and unfolding the functions EQUAL, LESSP, and ALL-NON-ZEROP, to:
T.
Case 9. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 1))
(ALL-NON-ZEROP '(1))).
However this again simplifies, appealing to the lemma
REMAINDER-OF-1, and unfolding the definition of EQUAL, to:
T.
Case 8. (IMPLIES
(AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-NON-ZEROP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which we again simplify, using linear arithmetic, rewriting with
REMAINDER-0-CROCK, DIFFERENCE-0, CDR-CONS, and CAR-CONS, and
opening up LESSP, REMAINDER, and ALL-NON-ZEROP, to:
(IMPLIES (AND ( LEQ (SUB1 P) (SUB1 I))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(NOT (EQUAL (INVERSE I P) 0))).
This simplifies again, using linear arithmetic, to:
T.
Case 7. (IMPLIES
(AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-NON-ZEROP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which we again simplify, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP NIL)),
which again simplifies, using linear arithmetic, rewriting with
N-Z-I-LEMMA and BOUNDED-INVERSE, and expanding the definitions of
PRIME, ZEROP, and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP NIL)).
However this again simplifies, using linear arithmetic, rewriting
with the lemma N-Z-I-LEMMA, and unfolding the definitions of ZEROP
and EQUAL, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 1))
(ALL-NON-ZEROP '(1))),
which again simplifies, unfolding EQUAL, NUMBERP, and ALL-NON-ZEROP,
to:
T.
Case 2. (IMPLIES
(AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-NON-ZEROP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, applying CDR-CONS and CAR-CONS, and
expanding the function ALL-NON-ZEROP, to:
T.
Case 1. (IMPLIES
(AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-NON-ZEROP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 98.227995 0.635026045 ]
ALL-NON-ZEROP-INVERSE-LIST
(PROVE-LEMMA BOUNDED-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(EQUAL J (DIFFERENCE P 2.)))
(ALL-LESSEQP (INVERSE-LIST I P) J))
((USE (BOUNDED-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
This conjecture simplifies, using linear arithmetic, applying
SUB1-NNUMBERP, DIFFERENCE-0, and DIFFERENCE-1, and unfolding the
functions PRIME, AND, IMPLIES, ZEROP, NOT, SUB1, EQUAL, LESSP,
DIFFERENCE, OR, INVERSE-LIST, and NUMBERP, to six new conjectures:
Case 6. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P)))
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
J)).
However this simplifies again, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P))))
(ALL-LESSEQP NIL J)).
This simplifies again, using linear arithmetic, applying
N-Z-I-LEMMA, PIGEON-HOLE-PRINCIPLE-LEMMA-2, and ADD1-SUB1, and
opening up ZEROP, EQUAL, LESSP, ALL-LESSEQP, MEMBER, and LISTP, to:
T.
Case 4. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P))))
(ALL-LESSEQP NIL J)),
which we again simplify, using linear arithmetic, rewriting with
N-Z-I-LEMMA, PIGEON-HOLE-PRINCIPLE-LEMMA-2, and ADD1-SUB1, and
unfolding the functions ZEROP, EQUAL, LESSP, ALL-LESSEQP, MEMBER,
and LISTP, to:
T.
Case 3. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P)))
(EQUAL I 1))
(ALL-LESSEQP '(1) J)).
But this simplifies again, applying PIGEON-HOLE-PRINCIPLE-LEMMA-2
and ADD1-SUB1, and unfolding the definitions of EQUAL, NUMBERP, CDR,
CAR, LISTP, ALL-LESSEQP, and MEMBER, to:
(IMPLIES (AND (LESSP (INVERSE 1 P) (SUB1 P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP 1 (SUB1 P)))
( LEQ 1 (SUB1 (SUB1 P)))),
which we again simplify, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL J (SUB1 (SUB1 P)))
(ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
J)
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-LESSEQP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
J)),
which again simplifies, applying CDR-CONS and CAR-CONS, and
expanding the function ALL-LESSEQP, to two new formulas:
Case 2.2.
(IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
(SUB1 (SUB1 P)))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
( LEQ I (SUB1 (SUB1 P)))).
This again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
(SUB1 (SUB1 P)))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
( LEQ (INVERSE I P) (SUB1 (SUB1 P)))),
which we again simplify, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P)))
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-LESSEQP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
J)).
But this simplifies again, using linear arithmetic, to:
T.
Q.E.D.
[ 90.283968 0.53803711 ]
BOUNDED-INVERSE-LIST
(PROVE-LEMMA SUBSETP-POSITIVES
(REWRITE)
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P)))
Name the conjecture *1.
We will try to prove it by induction. Two inductions are
suggested by terms in the conjecture. However, they merge into one
likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (ZEROP N) (P N P))
(IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
(P N P))
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(MEMBER N (INVERSE-LIST (SUB1 N) P))
(P (SUB1 N) P))
(P N P))
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(NOT (MEMBER N (INVERSE-LIST (SUB1 N) P)))
(P (SUB1 N) P))
(P N P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of
ZEROP can be used to prove that the measure (COUNT N) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces four new formulas:
Case 4. (IMPLIES (ZEROP N)
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))).
This simplifies, opening up the definitions of ZEROP, POSITIVES,
EQUAL, INVERSE-LIST, and SUBSETP, to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))),
which we simplify, opening up ZEROP, POSITIVES, NUMBERP, EQUAL,
INVERSE-LIST, and SUBSETP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(MEMBER N (INVERSE-LIST (SUB1 N) P))
(SUBSETP (POSITIVES (SUB1 N))
(INVERSE-LIST (SUB1 N) P)))
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))),
which we simplify, rewriting with CDR-CONS and CAR-CONS, and
unfolding the functions ZEROP, POSITIVES, INVERSE-LIST, and SUBSETP,
to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(NOT (MEMBER N (INVERSE-LIST (SUB1 N) P)))
(SUBSETP (POSITIVES (SUB1 N))
(INVERSE-LIST (SUB1 N) P)))
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))).
This simplifies, rewriting with DIFFERENCE-1, SUBSETP-CONS,
CDR-CONS, and CAR-CONS, and expanding ZEROP, POSITIVES,
INVERSE-LIST, DIFFERENCE, EQUAL, NUMBERP, SUB1, INVERSE, MEMBER,
and SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 10.0020182 0.301985677 ]
SUBSETP-POSITIVES
(PROVE-LEMMA INVERSE-1
(REWRITE)
(IMPLIES (LESSP 1. P)
(EQUAL (INVERSE 1. P) 1.)))
WARNING: Note that the rewrite rule INVERSE-1 will be stored so as
to apply only to terms with the nonrecursive function symbol INVERSE.
This formula simplifies, applying the lemmas REMAINDER-OF-1, EXP-OF-1,
and DIFFERENCE-1, and opening up DIFFERENCE, EQUAL, NUMBERP, SUB1,
REMAINDER, and INVERSE, to:
(IMPLIES (AND (LESSP 1 P) (NOT (EQUAL P 2)))
(NOT (EQUAL P 1))).
This simplifies again, using linear arithmetic, to:
T.
Q.E.D.
[ 2.28802082 0.06398112 ]
INVERSE-1
(PROVE-LEMMA A-D-I-L-LEMMA1
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P) 0.))
(LESSP I P)
(MEMBER J (INVERSE-LIST I P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
((USE (INVERSE-OF-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
This conjecture simplifies, rewriting with REMAINDER-WRT-12 and
REMAINDER-WRT-1, and opening up the functions PRIME, NOT, AND,
IMPLIES, ZEROP, EQUAL, REMAINDER, LESSP, INVERSE-LIST, OR, SUB1, and
NUMBERP, to nine new formulas:
Case 9. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ P (SUB1 I))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(MEMBER J (INVERSE-LIST (SUB1 I) P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))).
This again simplifies, using linear arithmetic, to:
T.
Case 8. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (REMAINDER (SUB1 I) P) 0)
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(MEMBER J (INVERSE-LIST (SUB1 I) P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))),
which we again simplify, using linear arithmetic, applying
INVERSE-OF-INVERSE, REMAINDER-0-CROCK, and DIFFERENCE-0, and
opening up PRIME, REMAINDER, EQUAL, INVERSE-LIST, LISTP, and MEMBER,
to:
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ P (SUB1 I))
(LESSP I P)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(MEMBER J (INVERSE-LIST (SUB1 I) P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J NIL))
(MEMBER (INVERSE J P) NIL)),
which again simplifies, using linear arithmetic, appealing to the
lemma N-Z-I-LEMMA, and unfolding the definitions of ZEROP, LESSP,
REMAINDER, and EQUAL, to:
T.
Case 6. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J NIL))
(MEMBER (INVERSE J P) NIL)),
which we again simplify, using linear arithmetic, rewriting with
N-Z-I-LEMMA and REMAINDER-0-CROCK, and opening up ZEROP and EQUAL,
to:
T.
Case 5. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(EQUAL I 1)
(MEMBER J '(1)))
(MEMBER (INVERSE J P) '(1))),
which again simplifies, applying INVERSE-1 and REMAINDER-OF-1, and
expanding the functions EQUAL, NUMBERP, CDR, CAR, LISTP, and MEMBER,
to:
T.
Case 4. (IMPLIES
(AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (REMAINDER (SUB1 I) P) 0)
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(MEMBER J
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))
(MEMBER (INVERSE J P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which we again simplify, using linear arithmetic, rewriting with
INVERSE-OF-INVERSE, REMAINDER-0-CROCK, DIFFERENCE-0, CDR-CONS, and
CAR-CONS, and expanding the definitions of PRIME, REMAINDER, EQUAL,
INVERSE-LIST, LISTP, and MEMBER, to three new conjectures:
Case 4.3.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (SUB1 I) 0)
(LESSP I P)
(NOT (EQUAL I 1))
(EQUAL J (INVERSE I P))
(NOT (EQUAL (INVERSE J P) I)))
(EQUAL (INVERSE J P) J)).
But this simplifies again, using linear arithmetic, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ P (SUB1 I))
(LESSP I P)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL J (INVERSE I P))
(NOT (EQUAL (INVERSE J P) I))
(NOT (EQUAL (INVERSE J P) J)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))).
But this simplifies again, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ P (SUB1 I))
(LESSP I P)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(MEMBER J (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (INVERSE J P) I))
(NOT (EQUAL (INVERSE J P) (INVERSE I P))))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))).
This simplifies again, using linear arithmetic, to:
T.
Case 3. (IMPLIES
(AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ P (SUB1 I))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(MEMBER J
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))
(MEMBER (INVERSE J P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))).
However this simplifies again, using linear arithmetic, to:
T.
Case 2. (IMPLIES
(AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(MEMBER J
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))
(MEMBER (INVERSE J P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, applying INVERSE-OF-INVERSE, CDR-CONS, and
CAR-CONS, and expanding the functions PRIME, REMAINDER, and MEMBER,
to:
T.
Case 1. (IMPLIES
(AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (MEMBER J (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(MEMBER J
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))
(MEMBER (INVERSE J P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, applying INVERSE-OF-INVERSE, CDR-CONS, and
CAR-CONS, and opening up the definitions of PRIME, REMAINDER, and
MEMBER, to the new formula:
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (MEMBER J (INVERSE-LIST (SUB1 I) P)))
(LESSP I P)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL J (INVERSE I P))
(NOT (EQUAL (INVERSE J P) I))
(NOT (EQUAL (INVERSE J P) J)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))),
which we again simplify, using linear arithmetic, applying the
lemma INVERSE-OF-INVERSE, and opening up the definitions of
REMAINDER and PRIME, to:
T.
Q.E.D.
[ 400.615967 0.85201823 ]
A-D-I-L-LEMMA1
(PROVE-LEMMA A-D-I-L-LEMMA2
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P) 0.))
(NOT (EQUAL (REMAINDER J P) 0.))
(LESSP I P)
(LESSP J P)
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
(MEMBER J (INVERSE-LIST I P)))
((USE (INVERSE-OF-INVERSE)
(A-D-I-L-LEMMA1 (J (INVERSE J P))))
(DISABLE INVERSE INVERSE-LIST INVERSE-OF-INVERSE
A-D-I-L-LEMMA1)))
This conjecture can be simplified, using the abbreviations NOT, PRIME,
IMPLIES, and AND, to:
(IMPLIES
(AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P)))
(IMPLIES (AND (PRIME P)
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP I P)
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))))
(MEMBER (INVERSE (INVERSE J P) P)
(INVERSE-LIST I P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER I P) 0))
(NOT (EQUAL (REMAINDER J P) 0))
(LESSP I P)
(LESSP J P)
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
(MEMBER J (INVERSE-LIST I P))).
This simplifies, using linear arithmetic, applying REMAINDER-0-CROCK
and N-Z-I-LEMMA, and expanding the definitions of PRIME, REMAINDER,
NOT, AND, IMPLIES, EQUAL, LESSP, and ZEROP, to:
T.
Q.E.D.
[ 45.877995 0.098990886 ]
A-D-I-L-LEMMA2
(PROVE-LEMMA A-D-I-L-LEMMA3
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(ALL-DISTINCT (INVERSE-LIST I P)))
((USE (A-D-I-L-LEMMA2 (J I) (I (SUB1 I)))
(NO-OTHER-INVOLUTIONS (J I)))
(DISABLE INVERSE)))
This conjecture can be simplified, using the abbreviations PRIME,
IMPLIES, and AND, to the goal:
(IMPLIES
(AND
(IMPLIES
(AND
(PRIME P)
(AND (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(IMPLIES (AND (PRIME P)
(AND (LESSP I (SUB1 P)) (LESSP 1 I)))
(NOT (EQUAL (INVERSE I P) I)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(ALL-DISTINCT (INVERSE-LIST I P))),
which simplifies, using linear arithmetic, applying the lemmas
REMAINDER-0-CROCK, DIFFERENCE-0, SUB1-NNUMBERP, and N-Z-I-LEMMA, and
expanding the definitions of PRIME, REMAINDER, NOT, LESSP, AND,
IMPLIES, SUB1, NUMBERP, EQUAL, INVERSE-LIST, ALL-DISTINCT, LISTP,
MEMBER, and ZEROP, to 43 new goals:
Case 43.(IMPLIES
(AND
(LESSP I 1)
(IMPLIES
(AND
(PRIME P)
(AND
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which we again simplify, using linear arithmetic, to:
T.
Case 42.(IMPLIES
(AND
(LESSP I 1)
(IMPLIES
(AND
(PRIME P)
(AND
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))).
However this simplifies again, using linear arithmetic, to:
T.
Case 41.(IMPLIES
(AND
(LESSP I 1)
(IMPLIES
(AND
(PRIME P)
(AND
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)).
This simplifies again, using linear arithmetic, applying
REMAINDER-0-CROCK and N-Z-I-LEMMA, and opening up LESSP, PRIME,
EQUAL, NOT, ZEROP, INVERSE-LIST, MEMBER, AND, IMPLIES, SUB1, and
ALL-DISTINCT, to:
T.
Case 40.(IMPLIES
(AND
(LESSP I 1)
(IMPLIES
(AND
(PRIME P)
(AND
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which we again simplify, using linear arithmetic, rewriting with
REMAINDER-0-CROCK, N-Z-I-LEMMA, and SUB1-NNUMBERP, and unfolding
the functions NUMBERP, EQUAL, LESSP, PRIME, NOT, REMAINDER, ZEROP,
INVERSE-LIST, MEMBER, AND, LISTP, IMPLIES, and ALL-DISTINCT, to:
T.
Case 39.(IMPLIES
(AND
(LESSP I 1)
(IMPLIES
(AND
(PRIME P)
(AND
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))).
But this simplifies again, using linear arithmetic, to:
T.
Case 38.(IMPLIES
(AND
(LESSP I 1)
(IMPLIES
(AND
(PRIME P)
(AND
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))).
However this simplifies again, using linear arithmetic, to:
T.
Case 37.(IMPLIES
(AND
(LESSP I 1)
(IMPLIES
(AND
(PRIME P)
(AND
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which we again simplify, using linear arithmetic, rewriting with
REMAINDER-0-CROCK and N-Z-I-LEMMA, and expanding the definitions of
LESSP, PRIME, SUB1, EQUAL, NOT, ZEROP, INVERSE-LIST, MEMBER, AND,
and IMPLIES, to:
T.
Case 36.(IMPLIES
(AND
(LESSP I 1)
(IMPLIES
(AND
(PRIME P)
(AND
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(AND (NOT (EQUAL (REMAINDER I P) 0))
(AND (LESSP (SUB1 I) P)
(AND (LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which we again simplify, using linear arithmetic, rewriting with
the lemmas SUB1-NNUMBERP, REMAINDER-0-CROCK, and N-Z-I-LEMMA, and
unfolding NUMBERP, EQUAL, LESSP, PRIME, NOT, REMAINDER, ZEROP,
INVERSE-LIST, MEMBER, AND, LISTP, IMPLIES, and ALL-DISTINCT, to:
T.
Case 35.(IMPLIES (AND ( LEQ 1 I)
( LEQ P (SUB1 I))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 34.(IMPLIES (AND ( LEQ 1 I)
( LEQ P (SUB1 I))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which we again simplify, using linear arithmetic, to:
T.
Case 33.(IMPLIES (AND ( LEQ 1 I)
( LEQ P (SUB1 I))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)).
But this simplifies again, using linear arithmetic, to:
T.
Case 32.(IMPLIES (AND ( LEQ 1 I)
( LEQ P (SUB1 I))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)).
But this simplifies again, using linear arithmetic, to:
T.
Case 31.(IMPLIES
(AND ( LEQ 1 I)
( LEQ P (SUB1 I))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))).
This simplifies again, using linear arithmetic, to:
T.
Case 30.(IMPLIES (AND ( LEQ 1 I)
( LEQ P (SUB1 I))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))).
However this simplifies again, using linear arithmetic, to:
T.
Case 29.(IMPLIES (AND ( LEQ 1 I)
( LEQ P (SUB1 I))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 28.(IMPLIES (AND ( LEQ 1 I)
( LEQ P (SUB1 I))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which we again simplify, using linear arithmetic, to:
T.
Case 27.(IMPLIES (AND ( LEQ 1 I)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 26.(IMPLIES (AND ( LEQ 1 I)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, expanding the functions LESSP, SUB1, EQUAL,
NUMBERP, and ALL-DISTINCT, to:
T.
Case 25.(IMPLIES (AND ( LEQ 1 I)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 24.(IMPLIES (AND ( LEQ 1 I)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which we again simplify, opening up the definitions of NUMBERP,
EQUAL, and LESSP, to:
T.
Case 23.(IMPLIES (AND ( LEQ 1 I)
( LEQ (SUB1 P) (SUB1 I))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which we again simplify, using linear arithmetic, to:
T.
Case 22.(IMPLIES (AND ( LEQ 1 I)
( LEQ (SUB1 P) (SUB1 I))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which we again simplify, using linear arithmetic, to:
T.
Case 21.(IMPLIES (AND ( LEQ 1 I)
( LEQ (SUB1 P) (SUB1 I))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which we again simplify, trivially, to:
T.
Case 20.(IMPLIES (AND ( LEQ 1 I)
( LEQ (SUB1 P) (SUB1 I))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which we again simplify, using linear arithmetic, to:
T.
Case 19.(IMPLIES
(AND ( LEQ 1 I)
( LEQ (SUB1 P) (SUB1 I))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which we again simplify, using linear arithmetic, to:
T.
Case 18.(IMPLIES (AND ( LEQ 1 I)
( LEQ (SUB1 P) (SUB1 I))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which we again simplify, using linear arithmetic, to:
T.
Case 17.(IMPLIES (AND ( LEQ 1 I)
( LEQ (SUB1 P) (SUB1 I))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)).
However this again simplifies, using linear arithmetic, to:
T.
Case 16.(IMPLIES (AND ( LEQ 1 I)
( LEQ (SUB1 P) (SUB1 I))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)).
But this again simplifies, using linear arithmetic, to:
T.
Case 15.(IMPLIES (AND ( LEQ 1 I)
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which we again simplify, using linear arithmetic, to:
T.
Case 14.(IMPLIES (AND ( LEQ 1 I)
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))).
This again simplifies, using linear arithmetic, applying INVERSE-1,
and expanding the functions LESSP, EQUAL, INVERSE-LIST, MEMBER,
SUB1, NUMBERP, and ALL-DISTINCT, to:
T.
Case 13.(IMPLIES (AND ( LEQ 1 I)
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)).
This again simplifies, using linear arithmetic, to:
T.
Case 12.(IMPLIES (AND ( LEQ 1 I)
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which we again simplify, opening up the definitions of NUMBERP,
EQUAL, and LESSP, to:
T.
Case 11.(IMPLIES
(AND ( LEQ 1 I)
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))).
But this simplifies again, using linear arithmetic, rewriting with
the lemmas NO-OTHER-INVOLUTIONS, CDR-CONS, and CAR-CONS, and
expanding the definitions of SUB1, NUMBERP, EQUAL, LESSP, PRIME,
MEMBER, and ALL-DISTINCT, to:
T.
Case 10.(IMPLIES (AND ( LEQ 1 I)
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, applying INVERSE-1,
and opening up the functions LESSP, SUB1, EQUAL, INVERSE-LIST, and
MEMBER, to:
T.
Case 9. (IMPLIES (AND ( LEQ 1 I)
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which we again simplify, using linear arithmetic, to:
T.
Case 8. (IMPLIES (AND ( LEQ 1 I)
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)).
However this simplifies again, expanding the functions NUMBERP,
EQUAL, and LESSP, to:
T.
Case 7. (IMPLIES (AND ( LEQ 1 I)
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND ( LEQ 1 I)
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))).
But this again simplifies, unfolding the definitions of LESSP,
EQUAL, INVERSE-LIST, and MEMBER, to:
T.
Case 5. (IMPLIES (AND ( LEQ 1 I)
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND ( LEQ 1 I)
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)).
This again simplifies, expanding the definitions of NUMBERP, EQUAL,
and LESSP, to:
T.
Case 3. (IMPLIES (AND ( LEQ 1 I)
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which we again simplify, unfolding LESSP, SUB1, EQUAL, INVERSE-LIST,
and MEMBER, to:
T.
Case 2. (IMPLIES (AND ( LEQ 1 I)
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)).
This again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND ( LEQ 1 I)
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, unfolding the functions NUMBERP, EQUAL, and
LESSP, to:
T.
Q.E.D.
[ 271.13812 2.216862 ]
A-D-I-L-LEMMA3
(PROVE-LEMMA ALL-DISTINCT-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I (SUB1 P)))
(ALL-DISTINCT (INVERSE-LIST I P)))
((USE (A-D-I-L-LEMMA3))
(INDUCT (POSITIVES I))
(DISABLE INVERSE)))
WARNING: the newly proposed lemma, ALL-DISTINCT-INVERSE-LIST, could
be applied whenever the previously added lemma A-D-I-L-LEMMA3 could.
This formula simplifies, applying SUB1-NNUMBERP, and opening up PRIME,
AND, INVERSE-LIST, IMPLIES, ZEROP, NOT, LESSP, ALL-DISTINCT, OR,
EQUAL, SUB1, and NUMBERP, to the following seven new goals:
Case 7. (IMPLIES
(AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))),
which we again simplify, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P)))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))).
However this again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES
(AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1)))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which we again simplify, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(EQUAL I 1))
(ALL-DISTINCT '(1))).
However this simplifies again, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ (SUB1 P) (SUB1 I))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1)))
(NOT (MEMBER I
(INVERSE-LIST (SUB1 I) P)))).
This simplifies again, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-DISTINCT NIL)),
which we again simplify, unfolding SUB1, EQUAL, INVERSE-LIST, and
ALL-DISTINCT, to:
T.
Case 1. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-DISTINCT NIL)),
which again simplifies, rewriting with SUB1-NNUMBERP, and opening
up the functions EQUAL, INVERSE-LIST, and ALL-DISTINCT, to:
T.
Q.E.D.
[ 78.2970705 0.326953124 ]
ALL-DISTINCT-INVERSE-LIST
(PROVE-LEMMA T-I-L-LEMMA1
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (TIMES A B) P) 1.)
(EQUAL (REMAINDER (TIMES A (TIMES B C)) P)
(REMAINDER C P)))
((USE (TIMES-MOD-3 (A (TIMES A B))
(B C)
(N P)))
(DISABLE TIMES-MOD-3)))
This formula can be simplified, using the abbreviations IMPLIES and
ASSOCIATIVITY-OF-TIMES, to:
(IMPLIES
(AND (EQUAL (REMAINDER (TIMES (REMAINDER (TIMES A B) P) C)
P)
(REMAINDER (TIMES A (TIMES B C)) P))
(EQUAL (REMAINDER (TIMES A B) P) 1))
(EQUAL (REMAINDER (TIMES A (TIMES B C)) P)
(REMAINDER C P))).
This simplifies, rewriting with TIMES-1, TIMES-ZERO2,
COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and opening up the
definitions of LESSP, EQUAL, and REMAINDER, to:
T.
Q.E.D.
[ 9.9609375 0.0600585938 ]
T-I-L-LEMMA1
(PROVE-LEMMA T-I-L-LEMMA
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1.)
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P)))
((USE (T-I-L-LEMMA1 (A I)
(B (INVERSE I P))
(C (TIMES-LIST (INVERSE-LIST (SUB1 I) P)))))
(DISABLE T-I-L-LEMMA1 INVERSE INVERSE-INVERTS)))
This conjecture simplifies, opening up EQUAL, IMPLIES, and
INVERSE-LIST, to the following four new goals:
Case 4. (IMPLIES
(AND
(EQUAL
(REMAINDER
(TIMES I
(TIMES (INVERSE I P)
(TIMES-LIST (INVERSE-LIST (SUB1 I) P))))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(EQUAL
(REMAINDER
(TIMES-LIST (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))),
which we again simplify, applying CDR-CONS and CAR-CONS, and
unfolding the function TIMES-LIST, to:
T.
Case 3. (IMPLIES
(AND
(EQUAL
(REMAINDER
(TIMES I
(TIMES (INVERSE I P)
(TIMES-LIST (INVERSE-LIST (SUB1 I) P))))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(EQUAL (REMAINDER (TIMES-LIST '(1)) P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))),
which we again simplify, rewriting with TIMES-1,
COMMUTATIVITY-OF-TIMES, and REMAINDER-OF-1, and unfolding the
definitions of SUB1, EQUAL, INVERSE-LIST, TIMES-LIST, NUMBERP,
INVERSE, TIMES, and REMAINDER, to:
T.
Case 2. (IMPLIES
(AND
(EQUAL
(REMAINDER
(TIMES I
(TIMES (INVERSE I P)
(TIMES-LIST (INVERSE-LIST (SUB1 I) P))))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(EQUAL I 0))
(EQUAL (REMAINDER (TIMES-LIST NIL) P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))).
This simplifies again, applying TIMES-1, COMMUTATIVITY-OF-TIMES,
TIMES-IDENTITY, and REMAINDER-OF-1, and opening up SUB1, EQUAL,
INVERSE-LIST, TIMES-LIST, LESSP, REMAINDER, INVERSE, and TIMES, to:
T.
Case 1. (IMPLIES
(AND
(EQUAL
(REMAINDER
(TIMES I
(TIMES (INVERSE I P)
(TIMES-LIST (INVERSE-LIST (SUB1 I) P))))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(NOT (NUMBERP I)))
(EQUAL (REMAINDER (TIMES-LIST NIL) P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))),
which we again simplify, rewriting with SUB1-NNUMBERP, TIMES-1,
COMMUTATIVITY-OF-TIMES, EQUAL-TIMES-0, REMAINDER-OF-1, and
REMAINDER-WRT-1, and unfolding the functions EQUAL, INVERSE-LIST,
TIMES-LIST, LESSP, and REMAINDER, to:
T.
Q.E.D.
[ 67.036002 0.26500651 ]
T-I-L-LEMMA
(PROVE-LEMMA T-I-L-LEMMA3
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P) 0.)))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P)))
((USE (INVERSE-INVERTS (J I)))
(DISABLE INVERSE INVERSE-LIST TIMES-LIST REMAINDER PRIME)))
This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES and
T-I-L-LEMMA, and unfolding the functions NOT, AND, and IMPLIES, to:
T.
Q.E.D.
[ 3.71402994 0.0240234374 ]
T-I-L-LEMMA3
(PROVE-LEMMA T-I-L-LEMMA4
(REWRITE)
(IMPLIES (LEQ I 1.)
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1.)))
Name the conjecture *1.
Perhaps we can prove it by induction. The recursive terms in
the conjecture suggest two inductions. However, they merge into one
likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (OR (EQUAL I 0) (NOT (NUMBERP I)))
(P I P))
(IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(P I P))
(IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(P (SUB1 I) P))
(P I P))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the
definitions of OR and NOT can be used to prove that the measure
(COUNT I) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme
generates four new conjectures:
Case 4. (IMPLIES (AND (OR (EQUAL I 0) (NOT (NUMBERP I)))
( LEQ I 1))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)),
which simplifies, opening up the definitions of NOT, OR, LESSP,
EQUAL, INVERSE-LIST, and TIMES-LIST, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(OR (EQUAL 1 0) (NOT (NUMBERP 1)))
( LEQ I 1))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)).
This simplifies, expanding the functions NOT, OR, EQUAL, and
NUMBERP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(LESSP 1 (SUB1 I))
( LEQ I 1))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)),
which we simplify, using linear arithmetic, to:
(IMPLIES (AND (LESSP I 1)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(LESSP 1 (SUB1 I))
( LEQ I 1))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)),
which again simplifies, unfolding the functions SUB1, NUMBERP,
EQUAL, LESSP, NOT, and OR, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
( LEQ I 1))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)).
This simplifies, appealing to the lemma DIFFERENCE-1, and opening
up NOT, OR, EQUAL, NUMBERP, LESSP, SUB1, INVERSE-LIST, DIFFERENCE,
REMAINDER, and INVERSE, to the following five new formulas:
Case 1.5.
(IMPLIES
(AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 2))
(NOT (NUMBERP P)))
(EQUAL (TIMES-LIST (CONS I
(CONS (REMAINDER (EXP I 0) P)
(INVERSE-LIST (SUB1 I) P))))
1)),
which we again simplify, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES
(AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 2))
(EQUAL P 0))
(EQUAL (TIMES-LIST (CONS I
(CONS (REMAINDER (EXP I 0) P)
(INVERSE-LIST (SUB1 I) P))))
1)),
which we again simplify, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES
(AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 2))
(NOT (EQUAL P 0))
(NUMBERP P))
(EQUAL
(TIMES-LIST
(CONS I
(CONS (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
(INVERSE-LIST (SUB1 I) P))))
1)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES
(AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL P 2))
(EQUAL
(TIMES-LIST (CONS I
(CONS I (INVERSE-LIST (SUB1 I) P))))
1)),
which we again simplify, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(EQUAL I 1))
(EQUAL (TIMES-LIST '(1)) 1)),
which we again simplify, unfolding EQUAL, NUMBERP, INVERSE-LIST,
TIMES-LIST, and SUB1, to:
T.
That finishes the proof of *1. Q.E.D.
[ 5.4028971 0.54111328 ]
T-I-L-LEMMA4
(PROVE-LEMMA TIMES-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1.))
((USE (T-I-L-LEMMA3) (T-I-L-LEMMA4))
(INDUCT (POSITIVES I))
(DISABLE INVERSE INVERSE-LIST TIMES-LIST T-I-L-LEMMA3
T-I-L-LEMMA4)))
This simplifies, rewriting with REMAINDER-WRT-12, REMAINDER-OF-1, and
REMAINDER-WRT-1, and opening up the definitions of PRIME, NOT, AND,
IMPLIES, SUB1, NUMBERP, EQUAL, LESSP, ZEROP, REMAINDER, and OR, to
three new conjectures:
Case 3. (IMPLIES
(AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL (SUB1 I) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P)
1)
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1)),
which again simplifies, opening up the definition of REMAINDER, to:
T.
Case 2. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL (SUB1 I) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ P (SUB1 I))
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1)).
However this simplifies again, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL (SUB1 I) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
( LEQ P (SUB1 I))
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1)).
This simplifies again, using linear arithmetic, to:
T.
Q.E.D.
[ 307.12689 0.175097656 ]
TIMES-INVERSE-LIST
(PROVE-LEMMA DELETE-X-LEAVE-A
(REWRITE)
(IMPLIES (AND (MEMBER A S) (NOT (EQUAL A X)))
(MEMBER A (DELETE X S))))
Name the conjecture *1.
Perhaps we can prove it by induction. The recursive terms in
the conjecture suggest two inductions. However, they merge into one
likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (NLISTP S) (P A X S))
(IMPLIES (AND (NOT (NLISTP S))
(EQUAL A (CAR S)))
(P A X S))
(IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL A (CAR S)))
(P A X (CDR S)))
(P A X S))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT S) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces four new formulas:
Case 4. (IMPLIES (AND (NLISTP S)
(MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))).
This simplifies, opening up the definitions of NLISTP and MEMBER,
to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP S))
(EQUAL A (CAR S))
(MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))),
which we simplify, rewriting with the lemma CAR-CONS, and unfolding
the functions NLISTP, MEMBER, and DELETE, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL A (CAR S)))
(NOT (MEMBER A (CDR S)))
(MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))).
This simplifies, opening up the functions NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL A (CAR S)))
(MEMBER A (DELETE X (CDR S)))
(MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))).
This simplifies, expanding NLISTP, MEMBER, and DELETE, to:
(IMPLIES (AND (LISTP S)
(NOT (EQUAL A (CAR S)))
(MEMBER A (DELETE X (CDR S)))
(MEMBER A (CDR S))
(NOT (EQUAL A X))
(NOT (EQUAL X (CAR S))))
(MEMBER A
(CONS (CAR S) (DELETE X (CDR S))))),
which we again simplify, rewriting with CDR-CONS and CAR-CONS, and
expanding the definition of MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 2.58916014 0.29684245 ]
DELETE-X-LEAVE-A
(PROVE-LEMMA DELETE-MEMBER-LEAVE-SUBSET
(REWRITE)
(IMPLIES (AND (SUBSETP R S) (NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))))
Name the conjecture *1.
Perhaps we can prove it by induction. The recursive terms in
the conjecture suggest four inductions. They merge into two likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP R) (P R X S))
(IMPLIES (AND (NOT (NLISTP R))
(MEMBER (CAR R) S)
(P (CDR R) X S))
(P R X S))
(IMPLIES (AND (NOT (NLISTP R))
(NOT (MEMBER (CAR R) S)))
(P R X S))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT R) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces five new formulas:
Case 5. (IMPLIES (AND (NLISTP R)
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))).
This simplifies, opening up the definitions of NLISTP, SUBSETP, and
MEMBER, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP R))
(MEMBER (CAR R) S)
(NOT (SUBSETP (CDR R) S))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))),
which we simplify, opening up NLISTP and SUBSETP, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP R))
(MEMBER (CAR R) S)
(MEMBER X (CDR R))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))),
which we simplify, unfolding NLISTP, SUBSETP, and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP R))
(MEMBER (CAR R) S)
(SUBSETP (CDR R) (DELETE X S))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))).
This simplifies, rewriting with the lemma DELETE-X-LEAVE-A, and
expanding NLISTP, SUBSETP, and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP R))
(NOT (MEMBER (CAR R) S))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))),
which we simplify, opening up NLISTP and SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 1.34401041 0.273990884 ]
DELETE-MEMBER-LEAVE-SUBSET
(PROVE-LEMMA ALL-LESSEQP-DELETE
(REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))))
.
Applying the lemma SUB1-ELIM, we now replace N by (ADD1 X) to
eliminate (SUB1 N). We rely upon the type restriction lemma noted
when SUB1 was introduced to constrain the new variable. This
generates three new conjectures:
Case 3. (IMPLIES (AND (EQUAL N 0)
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))).
However this simplifies, opening up the definition of SUB1, to:
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L 0))
(ALL-LESSEQP (DELETE 0 L) 0)),
which we would normally push and work on later by induction. But
if we must use induction to prove the input conjecture, we prefer
to induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let us consider:
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))),
which we named *1 above. We will try to prove it by induction. The
recursive terms in the conjecture suggest three inductions. However,
they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP L) (P N L))
(IMPLIES (AND (NOT (NLISTP L)) (P N (CDR L)))
(P N L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to prove that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme produces
the following four new formulas:
Case 4. (IMPLIES (AND (NLISTP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))).
This simplifies, applying PIGEON-HOLE-PRINCIPLE-LEMMA-2,
DELETE-NON-MEMBER, and ADD1-SUB1, and unfolding the functions
NLISTP, ALL-DISTINCT, ALL-LESSEQP, and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))),
which we simplify, expanding the definitions of NLISTP and
ALL-DISTINCT, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) N))
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))),
which we simplify, unfolding NLISTP, ALL-DISTINCT, and ALL-LESSEQP,
to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))).
This simplifies, expanding NLISTP, ALL-DISTINCT, ALL-LESSEQP, and
DELETE, to two new conjectures:
Case 1.2.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
( LEQ (CAR L) N)
(ALL-LESSEQP (CDR L) N)
(NOT (EQUAL N (CAR L))))
(ALL-LESSEQP (CONS (CAR L) (DELETE N (CDR L)))
(SUB1 N))).
However this again simplifies, rewriting with the lemmas CDR-CONS
and CAR-CONS, and unfolding the definition of ALL-LESSEQP, to the
formula:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
( LEQ (CAR L) N)
(ALL-LESSEQP (CDR L) N)
(NOT (EQUAL N (CAR L))))
( LEQ (CAR L) (SUB1 N))),
which we again simplify, using linear arithmetic, to the
following three new conjectures:
Case 1.2.3.
(IMPLIES (AND (NOT (NUMBERP (CAR L)))
(LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
( LEQ (CAR L) N)
(ALL-LESSEQP (CDR L) N)
(NOT (EQUAL N (CAR L))))
( LEQ (CAR L) (SUB1 N))),
which again simplifies, unfolding the definition of LESSP, to:
T.
Case 1.2.2.
(IMPLIES (AND (NOT (NUMBERP N))
(LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
( LEQ (CAR L) N)
(ALL-LESSEQP (CDR L) N)
(NOT (EQUAL N (CAR L))))
( LEQ (CAR L) (SUB1 N))),
which again simplifies, applying SUB1-NNUMBERP, and opening up
the function LESSP, to:
T.
Case 1.2.1.
(IMPLIES (AND (NUMBERP N)
(NUMBERP (CAR L))
(LISTP L)
(ALL-LESSEQP (DELETE (CAR L) (CDR L))
(SUB1 (CAR L)))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
( LEQ (CAR L) (CAR L))
(ALL-LESSEQP (CDR L) (CAR L))
(NOT (EQUAL (CAR L) (CAR L))))
( LEQ (CAR L) (SUB1 (CAR L)))).
This simplifies again, trivially, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
( LEQ (CAR L) N)
(ALL-LESSEQP (CDR L) N)
(EQUAL N (CAR L)))
(ALL-LESSEQP (CDR L) (SUB1 N))).
But this simplifies again, applying DELETE-NON-MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 6.2839193 0.637076825 ]
ALL-LESSEQP-DELETE
(PROVE-LEMMA POSITIVES-BOUNDED
(REWRITE)
(IMPLIES (LESSP N M)
(NOT (MEMBER M (POSITIVES N)))))
This formula can be simplified, using the abbreviations
MEMBER-POSITIVES, NOT, and IMPLIES, to:
(IMPLIES (AND (LESSP N M)
(NOT (EQUAL M 0))
(NUMBERP M))
( LEQ (ADD1 N) M)).
This simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.15 0.0380208334 ]
POSITIVES-BOUNDED
(PROVE-LEMMA SUBSETP-POSITIVES-DELETE
(REWRITE)
(IMPLIES (SUBSETP (POSITIVES N) L)
(SUBSETP (POSITIVES (SUB1 N))
(DELETE N L))))
This formula simplifies, applying DELETE-MEMBER-LEAVE-SUBSET and
SUB1-NNUMBERP, and expanding the definitions of POSITIVES, SUB1,
MEMBER, and LISTP, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(SUBSETP (CONS N (POSITIVES (SUB1 N)))
L))
(SUBSETP (POSITIVES (SUB1 N))
(DELETE N L))).
But this simplifies again, using linear arithmetic, rewriting with
CDR-CONS, CAR-CONS, POSITIVES-BOUNDED, and DELETE-MEMBER-LEAVE-SUBSET,
and unfolding the definition of SUBSETP, to:
T.
Q.E.D.
[ 1.43499349 0.063997396 ]
SUBSETP-POSITIVES-DELETE
(PROVE-LEMMA NONZEROP-LESSEQP-ZERO
(REWRITE)
(IMPLIES (AND (ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))))
WARNING: Note that NONZEROP-LESSEQP-ZERO contains the free variable
N which will be chosen by instantiating the hypothesis (ZEROP N).
This formula simplifies, expanding the definition of ZEROP, to the
following two new formulas:
Case 2. (IMPLIES (AND (EQUAL N 0)
(ALL-LESSEQP L 0)
(ALL-NON-ZEROP L))
(NOT (LISTP L))).
This simplifies again, obviously, to:
(IMPLIES (AND (ALL-LESSEQP L 0)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which we will name *1.
Case 1. (IMPLIES (AND (NOT (NUMBERP N))
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which we would usually push and work on later by induction. But if
we must use induction to prove the input conjecture, we prefer to
induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let us consider:
(IMPLIES (AND (ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
named *1 above. We will try to prove it by induction. The recursive
terms in the conjecture suggest two inductions. However, they merge
into one likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (NLISTP L) (P L N))
(IMPLIES (AND (NOT (NLISTP L)) (P (CDR L) N))
(P L N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to prove that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme leads to
four new goals:
Case 4. (IMPLIES (AND (NLISTP L)
(ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))).
This simplifies, unfolding the definition of NLISTP, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) N))
(ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which we simplify, unfolding the functions NLISTP, ZEROP,
ALL-NON-ZEROP, ALL-LESSEQP, and LESSP, to:
(IMPLIES (AND (NOT (ALL-LESSEQP (CDR L) N))
(EQUAL N 0)
(ALL-LESSEQP L 0)
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L)))
(NOT (LISTP L))),
which again simplifies, expanding the definitions of LESSP, EQUAL,
and ALL-LESSEQP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-NON-ZEROP (CDR L)))
(ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which we simplify, unfolding NLISTP, ZEROP, ALL-NON-ZEROP,
ALL-LESSEQP, LESSP, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(NOT (LISTP (CDR L)))
(ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which simplifies, unfolding the definitions of NLISTP, ZEROP,
ALL-NON-ZEROP, ALL-LESSEQP, LESSP, and EQUAL, to:
(IMPLIES (AND (NOT (LISTP (CDR L)))
(EQUAL N 0)
(ALL-LESSEQP L 0)
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L)))
(NOT (LISTP L))).
However this again simplifies, opening up LESSP, EQUAL, and
ALL-LESSEQP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 3.53398436 0.401009116 ]
NONZEROP-LESSEQP-ZERO
(DEFN PIGEONHOLE2-INDUCTION
(L N)
(IF (ZEROP N)
T
(PIGEONHOLE2-INDUCTION (DELETE N L)
(SUB1 N))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition
of ZEROP establish that the measure (COUNT N) decreases according to
the well-founded relation LESSP in each recursive call. Hence,
PIGEONHOLE2-INDUCTION is accepted under the principle of definition.
Note that (TRUEP (PIGEONHOLE2-INDUCTION L N)) is a theorem.
[ 0.41201172 0.0439778646 ]
PIGEONHOLE2-INDUCTION
(PROVE-LEMMA PIGEONHOLE2
(REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N)
(SUBSETP (POSITIVES N) L))
(PERM (POSITIVES N) L))
((INDUCT (PIGEONHOLE2-INDUCTION L N))))
This conjecture can be simplified, using the abbreviations ZEROP,
IMPLIES, NOT, OR, and AND, to two new conjectures:
Case 2. (IMPLIES (AND (ZEROP N)
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N)
(SUBSETP (POSITIVES N) L))
(PERM (POSITIVES N) L)).
This simplifies, opening up the functions ZEROP, POSITIVES, LISTP,
SUBSETP, and PERM, to two new formulas:
Case 2.2.
(IMPLIES (AND (EQUAL N 0)
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))).
This again simplifies, clearly, to:
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which we will name *1.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))),
which we will name *2.
Case 1. (IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES (AND (ALL-DISTINCT (DELETE N L))
(AND (ALL-NON-ZEROP (DELETE N L))
(AND (ALL-LESSEQP (DELETE N L) (SUB1 N))
(SUBSETP (POSITIVES (SUB1 N))
(DELETE N L)))))
(PERM (POSITIVES (SUB1 N))
(DELETE N L)))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N)
(SUBSETP (POSITIVES N) L))
(PERM (POSITIVES N) L)).
This simplifies, rewriting with the lemmas ALL-DISTINCT-DELETE,
ALL-NON-ZEROP-DELETE, ALL-LESSEQP-DELETE, SUBSETP-POSITIVES-DELETE,
CDR-CONS, and CAR-CONS, and unfolding the functions AND, IMPLIES,
POSITIVES, SUBSETP, and PERM, to:
T.
So next consider:
(IMPLIES (AND (NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))),
named *2 above. Let us appeal to the induction principle. Three
inductions are suggested by terms in the conjecture. However, they
merge into one likely candidate induction. We will induct according
to the following scheme:
(AND (IMPLIES (NLISTP L) (P L N))
(IMPLIES (AND (NOT (NLISTP L)) (P (CDR L) N))
(P L N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to show that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme leads to
five new formulas:
Case 5. (IMPLIES (AND (NLISTP L)
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))),
which simplifies, expanding the definition of NLISTP, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))),
which we simplify, unfolding NLISTP and ALL-DISTINCT, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-NON-ZEROP (CDR L)))
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))),
which simplifies, unfolding the definitions of NLISTP, ALL-DISTINCT,
and ALL-NON-ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) N))
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))).
This simplifies, unfolding the definitions of NLISTP, ALL-DISTINCT,
ALL-NON-ZEROP, ALL-LESSEQP, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(NOT (LISTP (CDR L)))
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))),
which we simplify, unfolding the definitions of NLISTP,
ALL-DISTINCT, MEMBER, ALL-NON-ZEROP, ALL-LESSEQP, and LESSP, to:
T.
That finishes the proof of *2.
So next consider:
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which we named *1 above. We will try to prove it by induction. The
recursive terms in the conjecture suggest three inductions. However,
they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP L) (P L))
(IMPLIES (AND (NOT (NLISTP L)) (P (CDR L)))
(P L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases
according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to five new
conjectures:
Case 5. (IMPLIES (AND (NLISTP L)
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))).
This simplifies, expanding the definition of NLISTP, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))).
This simplifies, opening up the functions NLISTP and ALL-DISTINCT,
to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-NON-ZEROP (CDR L)))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))).
This simplifies, opening up the functions NLISTP, ALL-DISTINCT, and
ALL-NON-ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) 0))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))).
This simplifies, expanding the definitions of NLISTP, ALL-DISTINCT,
ALL-NON-ZEROP, ALL-LESSEQP, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(NOT (LISTP (CDR L)))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which we simplify, opening up the functions NLISTP, ALL-DISTINCT,
MEMBER, ALL-NON-ZEROP, ALL-LESSEQP, EQUAL, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 5.9069336 1.62304688 ]
PIGEONHOLE2
(PROVE-LEMMA PERM-POSITIVES-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2.)))
(PERM (POSITIVES I)
(INVERSE-LIST I P))))
This formula can be simplified, using the abbreviations PRIME, AND,
and IMPLIES, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL I (DIFFERENCE P 2)))
(PERM (POSITIVES I)
(INVERSE-LIST I P))).
This simplifies, using linear arithmetic, rewriting with DIFFERENCE-1,
SUBSETP-POSITIVES, BOUNDED-INVERSE-LIST, ALL-NON-ZEROP-INVERSE-LIST,
ALL-DISTINCT-INVERSE-LIST, and PIGEONHOLE2, and opening up the
definitions of SUB1, NUMBERP, EQUAL, DIFFERENCE, and PRIME, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (SUB1 P) 0))
(PERM (POSITIVES (DIFFERENCE P 2))
(INVERSE-LIST (DIFFERENCE P 2) P))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 4.4809896 0.101985677 ]
PERM-POSITIVES-INVERSE-LIST
(PROVE-LEMMA INVERSE-LIST-FACT
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2.)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
(FACT I)))
((USE (TIMES-LIST-EQUAL-FACT (N I)
(L (INVERSE-LIST I P))))
(DISABLE INVERSE-LIST)))
This conjecture can be simplified, using the abbreviations PRIME, AND,
and IMPLIES, to:
(IMPLIES (AND (IMPLIES (PERM (POSITIVES I)
(INVERSE-LIST I P))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
(FACT I)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
(FACT I))),
which simplifies, rewriting with DIFFERENCE-1 and
PERM-POSITIVES-INVERSE-LIST, and opening up the functions SUB1,
NUMBERP, EQUAL, DIFFERENCE, PRIME, and IMPLIES, to:
T.
Q.E.D.
[ 3.91090494 0.068098959 ]
INVERSE-LIST-FACT
(PROVE-LEMMA W-T-LEMMA
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2.)))
(EQUAL (REMAINDER (FACT I) P) 1.))
((USE (TIMES-INVERSE-LIST))))
This formula can be simplified, using the abbreviations PRIME, AND,
and IMPLIES, to:
(IMPLIES
(AND (IMPLIES (AND (PRIME P) (LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (REMAINDER (FACT I) P) 1)).
This simplifies, appealing to the lemmas DIFFERENCE-1 and
INVERSE-LIST-FACT, and expanding PRIME, SUB1, NUMBERP, EQUAL,
DIFFERENCE, AND, and IMPLIES, to:
(IMPLIES (AND ( LEQ P (SUB1 (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
1)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (SUB1 P) 0)
( LEQ P (SUB1 (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
1)),
which we again simplify, using linear arithmetic, to:
T.
Q.E.D.
[ 64.190006 0.125032552 ]
W-T-LEMMA
(PROVE-LEMMA WILSON-THM NIL
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (FACT (SUB1 P)) P)
(SUB1 P)))
((USE (W-T-LEMMA (I (SUB1 (SUB1 P))))
(THM-55-SPECIALIZED-TO-PRIMES (M (SUB1 P))
(X (FACT (SUB1 (SUB1 P))))
(Y 1.)))
(DISABLE W-T-LEMMA THM-55-SPECIALIZED-TO-PRIMES)))
This conjecture can be simplified, using the abbreviations PRIME,
IMPLIES, and AND, to the new conjecture:
(IMPLIES
(AND
(IMPLIES (AND (PRIME P)
(EQUAL (SUB1 (SUB1 P))
(DIFFERENCE P 2)))
(EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
1))
(IMPLIES
(AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 P) P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES (SUB1 P)
(FACT (SUB1 (SUB1 P))))
P)
(REMAINDER (TIMES (SUB1 P) 1) P))
(EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
(REMAINDER 1 P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (FACT (SUB1 P)) P)
(SUB1 P))).
This simplifies, using linear arithmetic, appealing to the lemmas
DIFFERENCE-1, REMAINDER-0-CROCK, REMAINDER-OF-1, DIFFERENCE-0,
TIMES-1, COMMUTATIVITY-OF-TIMES, INVERSE-1, and B-I-LEMMA2, and
expanding PRIME1, DIVIDES, PRIME, SUB1, NUMBERP, EQUAL, DIFFERENCE,
AND, IMPLIES, NOT, FACT, TIMES, LESSP, and REMAINDER, to:
(IMPLIES (AND (EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
1)
( LEQ (SUB1 P) (SUB1 (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(NOT (EQUAL (SUB1 P) 0))
(LESSP (SUB1 P) (SUB1 (SUB1 P)))
(PRIME1 P (SUB1 (SUB1 P))))
(EQUAL (REMAINDER (TIMES (SUB1 P)
(FACT (SUB1 (SUB1 P))))
P)
(SUB1 P))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 129.817024 0.15498047 ]
WILSON-THM
SYSTEM
[ 0.0 0.0 ]BASIS.LISP.
GENFACT.LISP.
EVENTS.LISP.
CODE-1-A.LISP.
CODE-B-D.LISP.
CODE-E-M.LISP.
CODE-N-R.LISP.
CODE-S-Z.LISP.
IO.LISP.
PPR.LISP.
Maclisp Version 2133
REDO-UNDONE-EVENTS completed. Here is FAILED-THMS:
NIL